Semantics and Verification of Hierarchical CRP Programs

Communicating Reactive Processes (CRP) paradigm unifies asynchronous and synchronous mechanisms of concurrent programming languages. As an example, CRP unifies Esterel and Hoare's Communicating Sequential Processes (CSP). It has been earlier shown that such a unification and in particular CRP can be used for the specification of hybrid systems and dynamic real-time systems. In this paper, we extend the CRP to support hierarchical refinement and describe a compositional semantics. Further, we show how verification can be done using the verification techniques and tools used for the verification of Esterel programs. We illustrate how a careful separation of Esterel and CSP mechanisms in CRP has enabled the use of the technique of verification by reductions for verification and illustrate the use of tools such as Auto/Autograph for the verification of CRP programs through the banker-teller example. 1 Introduction Programming languages that have been used for real-time programming can be ..