Symbolic Semantics for CSP

Communicating Sequential Processes (CSP) is a well-known formal language for describing concur- rent systems. Brookes, Hoare and Roscoe [2] have given a transition semantics for CSP that underlies common approaches to model checking properties of CSP programs. In this paper, we present a gen- eralized transition semantics of CSP, which we call HCSP, that merges the original transition system with ideas from Floyd-Hoare Logic and symbolic computation. This generalized semantics is shown to be sound and complete with respect to the original trace semantics. Traces in our system are sym- bolic representations of families of traces as given by the original semantics. This more compact representation allows us to expand the original CSP systems to effectively model check some CSP programs which are difficult for other CSP systems to analyze. In particular, our system can han- dle certain classes of non-deterministic choices as a single transition, while the original semantics would treat each choice separately, possibly leading to large or unbounded case analyses. All work described in this paper has been carried out in the theorem prover Isabelle. This then provides us with a framework for automated and interactive analysis of CSP processes. It also give us the ability to extract Ocaml code for an HCSP-based simulator directly from Isabelle.NSF 0917218NASA Contract NNA10DE79Cunpublishednot peer reviewe