%T Towards Guaranteeing Process Oriented Program Behaviour
%A  Frederick R. M. Barnes
%E Peter H. Welch,  S. Stepney,  F.A.C Polack,  Frederick R. M. Barnes,  Alistair A. McEwan,  G. S. Stiles,  Jan F. Broenink,  Adam T. Sampson
%B Communicating Process Architectures 2008
%X Though we have language guarantees for avoiding
   race\-hazards, and
design\-rules and formal\-methods for
   guaranteeing freedom from
deadlock, livelock and starvation,
   the work involved in checking the
latter typically
   discourages their use. This talk briefly examines a
new
   approach to guaranteeing process behaviour in occam\-π,
   that
removes most, if not all, of the leg\-work involved in
   checking
programs manually – a process that itself is
   error prone.
Behaviour specifications are given in\-program,
   that our experimental
compiler checks against the actual
   implementation. Furthermore, the
compiler is capable of
   generating the behavioural specification of any
process,
   which it does using a CSP\-like language, for use
   with
separate compilation or for other formal verification.