School of
Information Technology and Electrical Engineering

Speaker: Dr Jin Song Dong - National University of Singapore
Seminar Date: Thu, 07/06/2012 - 10:00
Venue: 78-420
Host: Ian Hayes and Roger Duke

Seminar Type:  ITEE Research Seminar


Popular  model checkers like SPIN, SMV and FDR are designed for specialised domain 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 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 a problem solving, planning and scheudling tool.  Since PAT was released 4 years ago, it has attracted 1400+ registered users form 300+ organisations worldwide.


Jin-Song Dong received Bachelor and PhD degrees in Computing from University of Queensland in 1992 and 1996.  From 1195-1998, he was a Research Scientist 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 and Innovations in Systems and Software Engineering.  His research interests include formal methods, software engineering, pervasive compuing and semantic technologies.  Some of his research work can be found at