Towards Expressive Specification and Efficient Model Checking

We share the views that specifications are preferably executable. In this tutorial, 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) which is a self-contained framework for system specification, simulation and verification. PAT supports a modeling language named CSP# (short for communicating sequential programs).