Paper Details

Communicating Process Architectures (CPA)
 Title: Towards Guaranteeing Process Oriented Program Behaviour
 Conference: Communicating Process Architectures 2008
 Authors: Frederick R. M. Barnes
Computing Laboratory, University of Kent
 Abstract: 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-pi, 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. 

BibTeX Entry