Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

7-2009

Abstract

High level specification languages like CSP use mathematical objects as abstractions to represent systems and processes. System behaviors are described as process expressions combined with compositional operators, which are associated with elegant algebraic laws for system analysis. 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 verification. We demonstrate that data operations can be modeled as terminating sequential programs, which can be composed using high-level compositional operators. CSP# is supported by the PAT model checker and has been applied to a number of systems.

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 2009 Third IEEE International Symposium on Theoretical Aspects of Software Engineering, Tianjin, China, July 29-31

First Page

127

Last Page

135

ISBN

9780769537573

Identifier

10.1109/TASE.2009.32

Publisher

IEEE

City or Country

Tianjin, China

Additional URL

https://doi.org/10.1109/TASE.2009.32

Download

Share

COinS