Derivation of an Operational Semantics for HOL-CSP
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].
For example, process specifications can be written in:
datatype 'a channel = left 'a | right 'a | mid 'a | ack
definition SYN :: "('a channel) set"
where "SYN ≡ (range mid) ∪ {ack}"
definition COPY :: "('a channel) process"
where "COPY ≡ (μ COPY. left`?`x → right`!`x → COPY)"
definition SEND :: "('a channel) process"
where "SEND ≡ (μ SEND. left`?`x → mid`!`x → ack → SEND)"
definition REC :: "('a channel) process"
where "REC ≡ (μ REC. mid`?`x → right`!`x → ack → REC)"
definition SYSTEM :: "('a channel) process"
where "SYSTEM ≡ ((SEND ⟦ SYN ⟧ REC) \\ SYN)"
and refinement relations be proven via a conventional fix point induction:
lemma "COPY ⊑ SYSTEM" proof ... qed
The purpose of this work is derive the operational semantics for CSP on the basis of the denotational definitions. The interest of this semantics is twofold:
- an operational semantics allows for symbolic execution of processes, which paves the way for simulations even for the case of infinite alphabets
- the equivalence proof would pave the way for the integration of the FDR model-checker, whose logs are basically constructed from operational semantic steps, and therefore combined model-checking and induction proofs.
Proceding
An operational semantics is presented by a new type of rules is proven inside Isabelle/HOL:
definition "P ⟶⇧a P'" where "P' = P after a"
where _after_ is an operator that produces from a process P the processes P' that is equal to the former after having engaged in the event a. In other words, _after_ is the inverse of the prefix:
a → P ⟶⇧a P
Based on this inverse relation, it is straight forward to reformulate the derived laws on processes as operational derivation rules; for example:
(a → P) ⟦S⟧ (a → Q) ⟶⇧a P ⟦S⟧ Q where a ∈ S
can algebraic property (already derived in HOL-CSP):
(a → P) ⟦S⟧ (a → Q) = (a → P⟦S⟧Q)
This results in the following
Workplan
- Define the _after_ operator and prove that it satisfies the process invariant
- Prove the inverse relation between _after_ operator wrt. prefix
- convert the ca. 100 algebraic laws into operational rules in the above style.
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
[5] A. W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 2005.