Abstract

System modeling is important and highly non-trivial. In general, specifications are not necessarily executable (Hayes and Jones 1989). Over the last decade, expressiveness is the main driving force in the specification language research community. Many integrated formal specification languages have been proposed in order to model systems with not only complicated control flows but also complex data structures and operations. However the downside of the high expressiveness is that it is extremely difficult to develop automatic reasoning tools for those languages. On the other hand, popular model checkers like SPIN, SMV and FDR are designed for specialized domains and are therefore based on restrictive modeling languages. We share the views that specifications are preferably executable (Fuchs 1992). In this talk, we introduce our latest effort on combining the expressiveness of integrated formal specification languages with the power of mechanical system analysis method like model checking. We present a process analysis toolkit (PAT , http://pat.comp.nus.edu.sg), which is a self-contained framework for system specification, simulation and verification. PAT supports a wide range of modeling languages including CSP# (short for communicating sequential programs), which shares similar design principle with integrated specification languages like TCOZ. Nonetheless, instead of relying on the Z language, CSP# mixes high-level modeling operators with low-level programs, for the purpose of flexible system modeling and efficient verification. In CSP#, data operations can be modeled as terminating sequential programs, which then can be composed using high-level compositional operators. The idea is to treat sequential terminating programs, which may indeed be C# programs, as internal events. The result is a highly expressive modeling language which covers many application domains.

Biography

Dr. Jin Song Dong received Bachelor (1st class hon) and PhD degrees in Computing from University of Queensland in 1992 and 1996. From 1995-1998, he was a Research Scientist at the Commonwealth Scientific and Industrial Research Organisation 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. His research interests include formal methods and software engineering. Some of his papers can be found at: http://www.comp.nus.edu.sg/~dongjs.