%T Adding Formal Verification to occam\-π
%A Peter H. Welch,  Jan Bækgaard Pedersen,  Frederick R. M. Barnes,  Carl G. Ritson,  Neil C.C. Brown
%E Peter H. Welch,  Adam T. Sampson,  Jan Bækgaard Pedersen,  Jon Kerridge,  Jan F. Broenink,  Frederick R. M. Barnes
%B Communicating Process Architectures 2011
%X This is a proposal for the formal verification of
   occam\-π
programs to be managed entirely within
   occam\-π.
The language is extended with qualifiers on
   types and processes
(to indicate relevance for verification
   and/or execution) and assertions
about refinement (including
   deadlock, livelock and determinism).
The compiler abstracts
   a set of CSPm equations and assertions,
delegates their
   analysis to the FDR2 model checker and reports back
in terms
   related to the occam\-π source.
The rules for mapping the
   extended occam\-π to CSPm are given.
The full range of
   CSPm assertions is accessible, with no knowledge of
CSP
   formalism required by the occam\-π programmer.  Programs
   are proved
just by <em>writing</em> and <em>compiling</em>
   programs.
A case\-study analysing a new (and elegant)
   solution to the <em>Dining
Philosophers</em> problem is
   presented.
Deadlock\-freedom for colleges with <em>any</em>
   number of philosphers
is established by verifying an
   induction argument (the base and
induction steps).
Finally,
   following guidelines laid down by Roscoe, the careful use
   of
<em>model compression</em> is demonstrated to verify
   directly the deadlock\-freedom
of an occam\-&pi; college
   with 10^2000 philosphers (in around 30 seconds).
All we need
   is a universe large enough to contain the computer
on which
   to run it.