Theorem proving support for CSP

Yoshinao Isobe

(Information Technology Research Institute Japan, visiting Swansea)

The recently developed CSP-Prover is an interactive theorem prover dedicated to refinement proofs within the process algebra CSP. It aims specifically at proofs on infinite state systems, which may also involve infinite non-determinism. For this reason, the CSP-Prover uses the stable failures model F as denotational semantics of CSP. Semantically, the CSP-Prover is based on the theory of complete metric spaces. Here, Banach's Fixed Point Theorem is used for two purposes: to prove the existence of fixed points, and to prove CSP refinement between two fixed points. An interesting detail in the context of the various CSP denotational semantics is that metric spaces are represented as so-called restriction spaces. Technically, the CSP-Prover is based on the generic theorem prover Isabelle, using the logic HOL-Complex. Within this logic, the syntax as well as the semantics of CSP is encoded, i.e., the CSP-Prover provides a deep encoding of CSP. This encoding follows a generic approach which makes it easy to re-use large parts of the encoding for other CSP models like the traces model T, or the failure-divergence model N, or even the various infinite traces models. At the end of the talk, the CSP-Prover will be demonstrated by a classical refinement example: the dining mathematicians.
Tuesday 23rd March 2004, 14:00
Robert Recorde Room
Department of Computer Science