Integrating Specification and Programs for System Modeling and Verification

摘要

High level specification languages like CSP use math ematical objects as abstractions to represent systems and processes. System behaviors are described as process ex pressions combined with compositional operators, which are associated with elegant algebraic laws for system anal ysis. Nonetheless, modeling systems with non-trivial data and functional aspects using CSP remains difficult. In this work, we propose a modeling language named CSP# (short for communicating sequential programs) which integrates high-level modeling operators with low-level procedural codes, for the purpose of efficient mechanical system ver ification. We demonstrate that data operations can be mod eled as terminating sequential programs, which can be com posed using high-level compositional operators. CSP# is supported by the PAT model checker and has been applied to a number of systems.