Converging CSP Specifications and C++ Programming via Selective Formalism

作     者：Gardner, William B 

作者机构：Department of Computing and Information Science University of Guelph Guelph Ont. NIG 2W1 Canada 

出 版 物：《ACM Transactions on Embedded Computing Systems》 (ACM Trans. Embedded Comput. Syst.)

年 卷 期：2005年第4卷第2期

页      面：302-330页

学科分类：0808[工学-电气工程] 08[工学] 0835[工学-软件工程] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主　　题：Design Executable specifications hardware/software codesign Languages object-oriented application frameworks Verification 

摘      要：CSP (communicating sequential processes) is a useful algebraic notation for creating a hierarchical behavioral specification for concurrent systems, due to its formal interprocess synchronization and communication semantics. CSP specifications are amenable to simulation and formal verification by model-checking tools. A translator has been created to synthesize C++ code from CSP for execution with an object-oriented framework called CSP++, thereby making CSP specifications directly executable. To overcome the drawback that CSP is neither a full-featured nor popular programming language, an approach called “selective formalism allows the use of CSP to be limited to specifying the control portion of a system, while the rest of its functionality is supplied in the form of C++ modules. These are activated through association with abstract events in the CSP specification. This is a new means of bringing convergence between a formal method and a popular programming language. It is believed that this methodology can be extended to hardware/software codesign for embedded systems. © 2005, ACM. All rights reserved.