Supporting Timed CSP Operators in CSP++

摘要

CSP++ is an open-source code synthesis tool consisting of a translator for a subset of CSPm and a C++ run-time framework. Version 5.0 now supports Timed CSP operators-timed interrupt, timed timeout, and timed prefix-as well as untimed variants of interrupt and timeout, with only 1% additional execution and memory overhead, though using interrupts is more costly. We describe the implementation and performance of the new operators, illustrating their use with a robot-vacuum cleaner case study. The tool thus becomes more useful for specifying the behaviour of soft real-time systems, and generating a timing-enabled executable program from its formal model.