Gardner Home | Research | Pages for Grad Students
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.
|
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. |
|||
|
Its major enhancement is the translation and implementation of five 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. |
Solovyov thesis1 |
||
|
|
|||
|
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 Snapshot of 2006 CSP++ team (L-to-R Gardner, Moore-Oliva, and Carter). |
@Tech report2 @Unpub report3 LFM08 paper4 CPA05 paper5 TECS paper8 |
||
|
Brought multiparty synchronization into full conformity with CSPm semantics. |
Doxsee thesis9 ECBS05 paper10 SAC05 poster11 |
||
|
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. |
|||
|
MEMOCODE paper12 Gardner thesis13 Wiley book14 |
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 ]
