Generation of Executable Code from HOL-CSP Processes

Description

The theory of Communicating Sequential Processes going back to Hoare and Roscoe is still today one of the reference theories for concurrent specification and computing. in Isabelle/HOL of the denotational semantics of the Failure/Divergence Model of CSP was undertaken; in particular, this model can cope with infinite alphabets, in contrast to model-checking approaches limited to finite ones. In this paper, we extend this theory to a significant degree by taking advantage of more powerful automation of modern Isabelle version, which came even closer to recent developments in the semantic foundation of CSP.

In prior work, CSP has been presented as conservative embedding in Isabelle/HOL; a theory that provides the definitions of the denotational semantics of the CSP operators and derives algebraic rules from these. It ia a characteristic feature of resulting theory Isabelle/HOL-CSP [1] that one can model and reason over processes with an infinite type that can be arbitrarily defined in HOL. A framework for semi-automated refinement proofs has also been provided [2].

The purpose of this work is to use code-generation techniques of the Isabelle system in order to generate efficient procedures that generate concrete random traces for a large set HOL-CSP processes.

The proposed approach consists in adapting the techniques described in [4] to Isabelle/HOL-CSP.

Bibliography

[1] Safouan Taha, Burkhart Wolff and Lina Ye:

    Isabelle/HOL-CSP, 2019.

[2] Safouan Taha, Burkhart Wolff and Lina Ye:

    The Isabelle/HOL-CSP Refinement Toolkit, 2020.

[3] Safouan Taha, Burkhart Wolff and Lina Ye:

    Philosophers may dine - definitively !, 
    PDF, iFM, Oct 2019.

[4] Simon Foster, Chung-Kil Hur, Jim Woodock:

    Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL.
    CONCUR 2021: 20:1-20:18