CSP++ is a tool that makes specifications written in CSPm executable and extensible. It is the basis for a technique called selective formalism, which allows part of a system to be designed in verifiable CSPm statements, automatically translated into C++, and linked with functions coded in C++. This paper describes in detail the subset of CSPm that can be accurately translated by CSPM, and how the CSP semantics are achieved by the runtime framework. It also explains restrictions that apply to coding in CSPm for software synthesis, and the rationale for those restrictions.
展开▼
