An updated theory for communicating sequential processes in Coq

Abstract

The ability of a system to perform operations simultaneously is known as concurrency. In concurrent systems, the extensive number of ways in which components can interact with one another significantly elevates the complexity of analysing the behaviour of such systems. CSP (Communicating Sequential Processes) introduces a convenient notation to accurately describe concurrent systems. Over the years, computational tools have been developed to enable the analysis of specifications in CSP, such as: the Failures-Divergence Refinement (FDR) tool, and theories in Isabelle (e.g., CSP-Prover, HOL-CSP). Previ- ously, an initial characterisation of CSP has been developed in Coq: CSPCoq. Here, we significantly extend the possibilities of using CSP to reason about concurrency in Coq. Now, we support compound communications, parametrised processes, and CSP operators that were not considered before. Well-formedness conditions are formalised in Coq and proof automation tactics are provided. The notions of Structured Operational Seman- tics (SOS), Labelled Transitions Systems (LTS), traces refinement, and deadlock of CSP specifications have also been captured in Coq. Graphical representation of LTSs is en- abled via the DOT language and the Graphviz visualisation software. Moreover, we have developed a VSCode extension that automatically converts specifications in CSPM (the machine-readable dialect of CSP) to CSPCoq.