Pervasive Model Checking

Abstract

Popular model checkers like SPIN, SMV and FDR are designed for specialized domains and are based on restrictive modeling languages. In this talk, we introduce our latest work on combining the expressiveness of state, event, real-time and probability based formalisms with the power of model checking. We present a process analysis toolkit (PAT, http://pat.comp.nus.edu.sg), which is a self-contained reasoning system for system specification, simulation and verification. PAT supports a wide range of modeling languages including CSP# (short for communicating sequential programs). The idea is to treat sequential terminating programs, which may indeed be C# programs, as CSP events. The result is a highly expressive modeling language which covers many application domains. PAT can also be used as a problem solving, planning and scheduling tool. Since PAT is released 4 years ago, it has attracted 2000+ registered users from 400+ organisations worldwide.

Short bio

Jin-Song Dong received Bachelor (1st hon.) and PhD degrees in Computing from University of Queensland in 1992 and 1996. From 1995-1998, he was Research Scientist at CSIRO in Australia. Since 1998 he has been in the School of Computing at the National University of Singapore (NUS) where he is currently Associate Professor and a member of PhD supervisors at NUS Graduate School. He is on the editorial board of Formal Aspects of Computing Journal and Innovations in Systems and Software Engineering, A NASA Journal. He has been general chair and program chair for a number of international conferences (including FM'14). Jin Song has been on visiting faculty at Oxford University (UK) and National Institute of Informatics (Japan). His research interests include formal methods, software engineering, pervasive computing and semantic technologies. Some of his research work can be found at: http://www.comp.nus.edu.sg/~dongjs

Resources

• talk slide