Formal specification and model checking

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. Our current research project is to combine the expressiveness of integrated formal specification languages with the power of mechanical system analysis method like model checking. We have developed a process analysis toolkit (PAT), which is a self-contained verification system 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. Recently real-time and probabilistic model checking modules have also been developed in PAT.

• TBD