Bridging CSP and C++ with Selective Formalism and Executable Specifications

CSP (Communicating Sequential Processes) is a useful algebraic notation for creating a hierarchical behavioural 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. 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. e activated through association with abstract events in the CSP specification. The target system is constructed using a framework called CSP++, which automatically translates CSP specifications into C++, thereby making CSP directly executable. Thus a bridge is built that allows a formal method to be combined with a popular programming language. It is believed that this methodo...

• Type: Conference
• Year: 2003
• Where: MEMOCODE
• Authors: William B. Gardner
• Keywords: CSP Specifications, Formal Interprocess Synchronization, MEMOCODE 2003, Popular Programming Language