Symbolic Semantics for CSP

Li, Liyi; Gunter, Elsa L.; Mansky, William

Permalink

https://hdl.handle.net/2142/44888 Copy

Description

Title

Symbolic Semantics for CSP

Author(s)

• Li, Liyi
• Gunter, Elsa L.
• Mansky, William

Issue Date

2013-06-18

Keyword(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.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/44888

Sponsor(s)/Grant Number(s)

• NSF 0917218
• NASA Contract NNA10DE79C

Owning Collections