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.
Jun Sun Yang Liu Jin Song Dong Chunqing Chen
National University of Singapore
国际会议
天津
英文
127-135
2009-07-29（万方平台首次上网日期，不代表论文的发表时间）