@InProceedings{Barnes08, title = "{T}owards {G}uaranteeing {P}rocess {O}riented {P}rogram {B}ehaviour", author= "Barnes, Frederick R. M.", editor= "Welch, Peter H. and Stepney, S. and Polack, F.A.C and Barnes, Frederick R. M. and McEwan, Alistair A. and Stiles, G. S. and Broenink, Jan F. and Sampson, Adam T.", pages = "--", booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2008", isbn= "978-1-58603-907-3", year= "2008", month= "sep", 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-\π, 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." }