A corrected failure-divergence model for CSP in Isabelle/HOL

We present a failure-divergence model for CSP following the concepts of [BR 85]. Its formal representation within higher order logic in the theorem prover Isabelle/HOL [Pau 94] revealed an error in the basic definition of CSP concerning the treatment of the termination symbol tick.A corrected model has been formally proven consistent with Isabelle/HOL. Moreover, the changed version maintains the essential algebraic properties of CSP. As a result, there is a proven correct implementation of a “CSP workbench” within Isabelle.