William B. Gardner
Abstract
CSP (communicating sequential processes) is a useful algebraic notation for creating a hierarchical behavioral 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. A translator has been created to synthesize C++ code from CSP for execution with an object-oriented framework called CSP++, thereby making CSP specifications directly executable. 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. This is a new means of bringing convergence between a formal method and a popular programming language. It is believed that this methodology can be extended to hardware/software codesign for embedded systems.
- Alagar, V. S. and Periyasamy, K. 1998. Specification of Software Systems. Springer-Verlag, Berlin. Google Scholar
- Arrowsmith, B. and McMillin, B. 1994. How to Program in CCSP. Technical Report CSC 94-20, Department of Computer Science, University of Missouri-Rolla.Google Scholar
- Balboni, A., Fornaciari, W., and Sciuto, D. 1996. Partitioning and exploration strategies in the TOSCA co-design flow. In Proceedings of Fourth International Workshop on Hardware/Software Codesign, Pittsburgh, March 1996. pp. 62--69. Google ScholarCross Ref
- Bergstra, J. A. and Klop, J. W. 1985. Algebra of Communicating Processes with abstraction. Theoretical Computer Science 37, 1, 77--121.Google ScholarCross Ref
- Carreras, C., López, J. C., López, M. L., Delgado-Kloos, C., Martínez, N., and Sánchez, L. 1996. A co-design methodology based on formal specification and high-level estimation. In Proceedings of Fourth International Workshop on Hardware/Software Codesign. Pittsburgh, March 1996, pp. 28--35. Google ScholarCross Ref
- Cheng, M. H. M. 1994. Communicating sequential processes: A synopsis. Department of Computer Science, University of Victoria, Canada.Google Scholar
- Davies, J. and Schneider, S. 1992. A Brief History of Timed CSP. Technical Report PRG-96, Programming Research Group, Oxford University.Google Scholar
- Engelschall, R. S. 2000. Portable multithreading: The signal stack trick for user-space thread creation. In Proceedings of USENIX Annual Technical Conference, San Diego, CA, June 2000. For software see GNU Portable Threads (pth): http://www.gnu.org/software/pth/ {as of 2/9/04}. Google Scholar
- EVES. 2003. EVES web site, ORA Canada. http://www.ora.on.ca/eves.html (as of 2/7/03).Google Scholar
- Fayad, M. E. and Schmidt, D. C. 1997. Object-oriented application frameworks. Communications of the ACM 40, 10, 32--38. Google ScholarDigital Library
- Fayad, M., Schmidt, D., and Johnson, R. (Ed.). 1999. Implementing Application Frameworks: Object-Oriented Frameworks at Work. Wiley, New York. Google Scholar
- FDR2. 2003. FDR2 web site, Formal Systems (Europe) Limited. http://www.fsel.com (as of 2/6/03).Google Scholar
- Gajski, D. D., Vahid, F., Narayan, S., and Gong, J. 1994. Specification and Design of Embedded Systems. PTR Prentice Hall, Englewood Cliffs, NJ. Google Scholar
- Gardner, W. 2000. CSP++: An object-oriented application framework for software synthesis from CSP specifications. Ph.D. dissertation, Department of Computer Science, University of Victoria, Canada. http://www.cis.uoguelph.ca/~wgardner/, Research link. Google Scholar
- Gardner, W. B. 2003. Bridging CSP and C++ with selective formalism and executable specifications. In First ACM & IEEE International Conference on Formal Methods and Models for Co-design (MEMOCODE '03), Mont St-Michel, France, June 2003. pp. 237--245. Google ScholarCross Ref
- Gardner, W. B. and Serra, M. 1999. CSP++: A framework for executable specifications. In Implementing Application Framework: Object-Oriented Framework at Work, M. Fayad, D. Schmidt, and R. Johnson, Eds. Wiley, New York.Google Scholar
- Hilderink, G., Broenink, J., Vervoort, W., and Bakkers, A. 1997. Communicating Java threads. In Proceedings of the 20th World Occam and Transputer User Group Technical Meeting, Enschede, The Netherlands. pp. 48--76.Google Scholar
- Hinchey, M. G. and Jarvis, S. A. 1995. Concurrent Systems: Formal Development in CSP. McGraw-Hill, New York. Google Scholar
- Hoare, C. A. R. 1985. Communicating Sequential Processes. Prentice Hall, Englewood Cliffs, NJ. Google Scholar
- Lea, D. 1996. Concurrent Programming in Java: Design Principles and Patterns. Addison-Wesley, Reading, MA. Google Scholar
- Lewis, B. and Berg, D. J. 1998. Multithreaded Programming with Pthreads. Sun Microsystems Press Prentice Hall, Palo Alto, CA. Google Scholar
- Lewis, T. (Ed.). 1995. Object-Oriented Application Frameworks. Manning Publications, Greenwich, CT.Google Scholar
- Logrippo, L., Faci, M., and Haj-Hussein, M. 1992. An introduction to LOTOS: Learning by examples. Computer Networks and ISDN Systems 23, 325--342. Google ScholarDigital Library
- Luqi and Goguen, J. A. 1997. Formal methods: Promises and problems. IEEE Software 14, 1 (Jan.), 73--85. Google ScholarDigital Library
- Matsuoka, S. and Yonezawa, A. 1993. Analysis of inheritance anomaly in object-oriented concurrent programming languages. In Research Directions in Concurrent Object-Oriented Programming, G. Agha, P. Wegner, and A. Yohezawa, Eds. MIT Press, Cambridge, MA, pp. 107--150. Google Scholar
- Milner, R. 1995. Communication and Concurrency. Prentice Hall, Englewood Cliffs, NJ. Google Scholar
- Reitzner, S. 1997. Splitting Synchronization from Algorithmic Behavior. Technical Report TR-I4-97-08, Friedrich-Alexander-University, Erlangen-Nürnberg, Germany.Google Scholar
- Roscoe, A. W. 1994. Model-checking CSP. In A Classical Mind: Essays in Honour of C. A. R. Hoare, A. W. Roscoe, Ed. Prentice Hall International Series in Computer Science. Prentice Hall, Englewood Cliffs, NJ, pp. 353--378. Google Scholar
- Roscoe, A. W. 1998. The Theory and Practice of Concurrency. Prentice Hall, Englewood Cliffs, NJ. Google Scholar
- Schneider, S. 2000. Concurrent and Real-time Systems: The CSP Approach. Wiley, New York. Google Scholar
- Silberschatz, A. and Galvin, P. B. 1998. Operating System Concepts, 5th ed. Addison-Wesley, Reading, MA. Google Scholar
- Sommerville, I. 1996. Software Engineering, 5th ed. Addison-Wesley, Reading, MA. Google Scholar
- Srinivasan, S. 1999. Design patterns in object-oriented frameworks. Computer 32, 2 (Feb.), 24--32. Google ScholarDigital Library
Index Terms
- Converging CSP specifications and C++ programming via selective formalism
Recommendations
Synthesis of C++ software for automated teller from CSPm specifications
SAC '05: Proceedings of the 2005 ACM symposium on Applied computingCSP++ 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 ...
Bridging CSP and C++ with Selective Formalism and Executable Specifications
MEMOCODE '03: Proceedings of the First ACM and IEEE International Conference on Formal Methods and Models for Co-DesignCSP (Communicating Sequential Processes) is a usefulalgebraic notation for creating a hierarchical behaviouralspecification for concurrent systems, due to its formalinterprocess synchronization and communication semantics.CSP specifications are amenable ...
Executable specifications of resource-bounded agents
Logical theories of intelligent (or rational) agents have been refined and improved over the past 20 years of research. Such logical theories are used in many ways, one of which is as the basis for executable agent specifications. Here, agents are ...
Comments