|
Published Articles >> Table of Contents >> Abstract
First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE’03)
p. 237
Bridging CSP and C++ with Selective Formalism and Executable Specifications
W. B. Gardner, Dept. of Computing & Information Science, Univ. of Guelph, Guelph, Ontario, Canada
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/MEMCOD.2003.1210108
Send link to a friend
| Abstract |
|
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.
These are 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 methodology
can be extended to hardware/software codesign.
|
 Additional Information
|
Citation:
W. B. Gardner,
"Bridging CSP and C++ with Selective Formalism and Executable Specifications,"
memocode,
p. 237,
First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE’03),
2003
|
|
