Files in this item



application/pdfgandALF2013.pdf (238kB)
(no description provided)PDF


Title:Symbolic Semantics for CSP
Author(s):Li, Liyi; Gunter, Elsa L.; Mansky, William
Subject(s):Symbolic evaluation
Process Algebras
Communicating Sequential Processes
Isabelle Theorem Prover
Abstract: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.
Issue Date:2013-06-18
Publication Status:unpublished
Peer Reviewed:not peer reviewed
Sponsor:NSF 0917218
NASA Contract NNA10DE79C
Date Available in IDEALS:2013-06-18

This item appears in the following Collection(s)

Item Statistics