×

Symbolic analysis tools for CSP. (English) Zbl 1432.68311

Ciobanu, Gabriel (ed.) et al., Theoretical aspects of computing – ICTAC 2014. 11th international colloquium, Bucharest, Romania, September 17–19, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8687, 295-313 (2014).
Summary: Communicating sequential processes (CSP) is a well-known formal language for describing concurrent systems, where transition semantics for it has been given by S. D. Brookes et al. [J. Assoc. Comput. Mach. 31, 560–599 (1984; Zbl 0628.68025)]. In this paper, we present trace refinement model analysis tools based on a generalized 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 symbolic 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 and efficiently model check some CSP programs that are difficult or impossible for other CSP systems to analyze. In particular, our system can handle 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 the 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 gives us the ability to extract Ocaml code for an HCSP-based simulator directly from Isabelle. Based on the HCSP semantics and traditional trace refinement, we develop an idea of symbolic trace refinement and build a model checker based on it. The model checker was transcribed by hand into Maude as automatic extraction of Maude code is not yet supported by the Isabelle system.
For the entire collection see [Zbl 1296.68006].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Citations:

Zbl 0628.68025

Software:

Maude; ProBE; OCaml; FDR3; FDR2; mCRL2
PDFBibTeX XMLCite
Full Text: DOI