POSTER PAPER Synthesis of C++ Software for Automated Teller from CSPm Specifications

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. Categories and Subject Descriptor