Synthesis of C++ software for automated teller from CSPm specifications
Stephen Doxsee, William B. Gardner · 2005
CSP++ is an object-oriented application framework for execution of CSP specifications that have been automatically translated into C++ source code by a tool called cspt. This approach makes CSP specifications directly executable, and extensible via the ability to incorporate user-coded functions. Designers can exploit "selective formalism" to code some system functionality in CSP for formal verification purposes, and other functionality directly in C++. The translator has now been enhanced to accept input in CSPm syntax, the same dialect processed by the commercial verification tool, FDR2, and we demonstrate this with a new ATM case study.