Gardner Home | Research | Pages for Grad Students

CSP++ Home

Last updated 7/Jun/12

CSP++ is a software synthesis tool for making specifications written in CSPm executable via C++. The cspt translator converts a CSPm file to C++ source code that is compiled together with the classes of the CSP++ object-oriented application framework (OOAF).

CSP++ in one page! [ PDF ]

It is intended that CSPm be used to create the formally-verifiable control backbone of a system, with CSPm events used to invoke user-coded functions written in C++. We call this mixture of formal notation and conventional programming language "selective formalism." CSPm specifications can be verified using the tools from Formal Systems (Europe) Ltd.

The run-time framework is based on GNU Pth portable threads. As of Version 4.2, CSP++ is Open Source under the GNU licenses GPL (cspt) and LGPL (OOAF). Contributors are advised to start reading with the two reports marked @ in the table below, since these are concise guides to the translator and OOAF, created for that purpose.

CSP++ is a project of the Modeling and Design Automation Group in Guelph's School of Computer Science under the direction of Dr. William Gardner.

Downloads and related publications

Version

Principal New Features

Downloads

Documents

5.1

This version's major feature is the creation of memory for user-coded functions on a per-CSP-process, i.e., thread-local, basis. This feature allows a complete process, whose interface consists of one or more events and/or channels, to be replaced by UCFs corresponding to that interface. (alpha stage, subject to change, see ChangeLog for instructions on enabling)

Other new additions include support for the translation of the CSPm modulo (%) and boolean (AND, OR, NOT) operators and associated keywords (true, false), as well as CSPm constants.

tar.gz package

coming summer 2012

5.0

Its major enhancement is the translation and implementation of five Timed CSP operators, which can be applicable to synthesis of soft realtime systems. They are: timed /t\ and untimed /\ interrupt, timed [t> and untimed [> timeout, and timed prefix -t-> .

A new Python script, fdrscript.py, collects the trace output generated by a CSP++ program, and massages it into a form accepted by FDR2, which can then use trace refinement to verify that the actual trace is valid for the original CSP specification.

Use 5.1

Solovyov thesis1

Demos

ATM: Automated Teller case study cited in ECBS paper.

DSS: Disk server case study cited in MEMOCODE paper and others, updated to CSPm syntax.

tar.gz package

 

4.2

This is the "micro" version (ucsp) of CSP++ that does away with the C++ STL and its large footprint (particularly formatted I/O) in the OO framework. V4.2 is the first public source code distro and is capable of installing via autoconf and automake on (hopefully) a wide variety of platforms. It also has a set of regression tests that are built/executed via "make check" (needs cppunit and boost).

A plug-in called cspdt was produced for Eclipse 3.2.0 that facilitates model-checking CSPm specifications and writing user-coded functions.

Snapshot of 2006 CSP++ team (L-to-R Gardner, Moore-Oliva, and Carter).

tar.gz package

Eclipse plug-in

@Tech report2

@Unpub report3

LFM08 paper4

CPA05 paper5

RSP05 paper6,7

TECS paper8

4.1

Brought multiparty synchronization into full conformity with CSPm semantics.

 

Doxsee thesis9

ECBS05 paper10

SAC05 poster11

4.0

This major release changes the input syntax from csp12 to CSPm, compatible with FDR2, ProBE, and Checker. It is now possible to take CSP files directly from verification with those commerical tools, and input them to cspt for software synthesis.

3.1 and earlier

 

 

MEMOCODE paper12

Gardner thesis13

Wiley book14

Gardner Home | Research | Pages for Grad Students


1. Yuriy Solovyov, "Extending CSP++ Framework with Timed CSP Operators," masters thesis, Dept. of Computing and Information Science, University of Guelph, 2008. [ PDF ]

2. W.B. Gardner, J. Moore-Oliva, J. Carter, A. Gumtie, Y. Solovyov, "CSP++: An Open Source Tool for Building Concurrent Applications from CSP Specifications," Department of Computing and Information Science, University of Guelph, TR-UG-CIS-2009-001. [ Dept PDF ]

3. W.B. Gardner, "Cspt: An Open Source Translator for CSPm," 2008. [ PDF ]

4. W.B. Gardner, "Getting Somewhat Formal with CSP and C++," Kristin Yvonne Rozier, Ed., Proc. of Sixth NASA Langley Formal Methods Workshop (LFM 2008), Newport News, VA, Apr. 30-May 2, pp. 23-25, NASA/CP-2008-215309. [ NASA PDF ]

5. W.B. Gardner, "CSP++: How Faithful to CSPm?," Communicating Process Architectures 2005 (WoTUG-27), Eindhoven, Sep. 18-21, Concurrent Systems Engineering Series, IOS Press, pp. 129-146. [ WoTUG PDF ]

6. John Carter, Ming Xu, W.B. Gardner, "Rapid Prototyping of Embedded Software Using Selective Formalism," 16th IEEE International Workshop on Rapid System Prototyping (RSP 2005), Montréal, June 8-10, pp. 99-104. [ PDF ]

7. John Carter, Ming Xu, W.B. Gardner, "Rapid Prototyping of Embedded Software Using Selective Formalism," Society of Manufacturing Engineers, Technical Paper No. TP06PUB28, www.sme.org. [ SME catalog ]

8. W.B. Gardner, "Converging CSP Specifications and C++ Programming via Selective Formalism," ACM Transactions on Embedded Computing Systems (TECS), Special Issue on Models and Methodologies for Co-Design of Embedded Systems, Vol. 4, No. 2, May 2005, pp. 302-330. [ DOI bookmark ]

9. Stephen Doxsee, "Reengineering CSP++ to Conform with CSPm Verification Tools," masters thesis, Dept. of Computing and Information Science, University of Guelph, 2005. [ PDF ]

10. S. Doxsee, W.B. Gardner, "Synthesis of C++ Software from Verifiable CSPm Specifications," 12th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2005), Greenbelt, MD, Apr. 4-5, pp. 193-201. [ PDF ]

11. S. Doxsee, W.B. Gardner, "Synthesis of C++ Software for Automated Teller from CSPm Specifications," 20th Annual ACM Symposium on Applied Computing (SAC `05), Software Engineering Track: Applications, Practices, and Tools, poster paper, Santa Fe, NM, Mar. 2005, pp.1565-1566. [ PDF ]

12. W.B. Gardner, "Bridging CSP and C++ with Selective Formalism and Executable Specifications," First ACM & IEEE International Conference on Formal Methods and Models for Co-design (MEMOCODE `03), Mont St-Michel, France, June 2003, pp. 237-245. [ PDF ]

13. William Gardner, "CSP++: An Object-Oriented Application Framework for Software Synthesis from CSP Specifications," Ph.D. dissertation, Dept. of Computer Science, University of Victoria, 2000. [ PDF ]

14. W.B. Gardner, M. Serra, "CSP++: A Framework for Executable Specifications," Implementing Application Frameworks: Object-Oriented Frameworks at Work, M. Fayad, D. Schmidt, & R. Johnson, Eds., John Wiley & Sons, chapter 9. [ publisher's website ]