Extending CSP++ framework with timed CSP operators.

摘要

Communicating Sequential Processes (CSP) is a formal process algebra used to specify and reason about concurrent systems. Timed CSP was subsequently created to add the capabilities of delays, timeouts, and interrupts, necessary for specifying systems with time-sensitive properties. The tool CSP++ was developed to make machine-readable CSPm specifications directly executable via automatic C++ code generation, and extensible via user-coded functions. Formerly, CSP++ could only synthesize CSP specifications abstracted from any timing information. In this work, CSP++ was extended to translate and synthesize specifications with new operators drawn from Timed CSP. These new features are demonstrated with a VAC Automated Cleaner case study and compared to other CSP-inspired programming libraries.