Synthesis of C++ software from verifiable CSPm specifications

Author

Doxsee, Stephen ; Gardner, W.B.

Author_Institution

Dept. of Comput. & Inf. Sci., Guelph Univ., Ont., Canada

fYear

2005

fDate

4-7 April 2005

Firstpage

193

Lastpage

201

Abstract

CSP++ is an object-oriented application framework for execution of CSP specifications that have been automatically synthesized into C++ source code by the cspt translator. We describe the tool\´s new capability of accepting input in CSPm syntax, the same dialect processed by the commercial verification tool, FDR2. Using a new ATM case study in CSPm, we give samples of generated code, and illustrate the use of "selective formalism" to code and verify some system functionality in CSP, and supply other functionality via user-coded C++ functions linked to events in the CSP specifications.

Keywords

C++ language; communicating sequential processes; formal specification; object-oriented programming; program verification; C++ language; communicating sequential process; formal specification; formal verification; object-oriented programming; verifiable CSPm specifications; Application software; Computer industry; Computer languages; Concurrent computing; Control system synthesis; Design automation; Formal specifications; Information science; Object oriented modeling; Software engineering;

fLanguage

English

Publisher

ieee

Conference_Titel

Engineering of Computer-Based Systems, 2005. ECBS '05. 12th IEEE International Conference and Workshops on the

Print_ISBN

0-7695-2308-0

Type

conf

DOI

10.1109/ECBS.2005.64

Filename

1409917