Supporting Selective Formalism in CSP++ with Process-Specific Storage

摘要

Communicating Sequential Processes (CSP) is a formal language whose primary purpose is to model and verify concurrent systems. The CSP++ toolset was created to realize the concept of selective formalism by making machine-readable CSPm specifications both executable (through automatic C++ code generation) and extensible (by allowing integration of C++ user-coded functions, UCFs). However, UCFs were limited by their inability to share data with each other, thus their application was constrained to solving simple problems in isolation. We extend CSP++ by providing UCFs in the same CSP process with safe access to a shared storage area, similar in concept and API to Pthreads' thread-local storage, enabling cooperation between them and granting them the ability to undertake more complex tasks without breaking the formalism of the underlying specification. Process-specific storage is demonstrated with a line-following robot case study, applying CSP++ in a soft real-time system. Also described is the Eclipse plug-in that supports the CSPm design flow.