Keywords: verification, semantics, distributed systems, message passing, value passing, lambda calculus, pi calculus
Start Date: 1 January 95 / Duration: 36 months
[ participants / contact]
The goal is to develop robust verification tools for distributed systems based on a solid theoretical understanding of their semantics. This requires both fundamental research into semantics for processes as well as the development of software tools using modern high-level languages such as Standard ML, and high-level interfaces to x-windows.
In previous work, a symbolic version of the standard bisimularity checking algorithm was developed for finite symbolic graphs. However, with this formalism there were difficulties to ensure that the symbolic graphs generated from the expressions of a value-passing process language are finite. The symbolic graphs have now been generalised to include information about assignments. The resulting formalism is much more powerful for capturing the intentional behaviour of value-passing processes, and the symbolic version of the bisimulation checking algorithm has been extended to this more general formalism.
The above mentioned results have been presented at the international conference CONCUR'96, which was held in Pisa in August 1996.
University of Sussex
University of Sussex, UK
Laboratoire d'Informatique de l'EcoleNormale Superieure, F
Institute of Software, Chinese Academy of Sciences, CHI
Prof. Matthew Hennessy
Tel: +44 1273 678 195
Fax: +44 1273 671 320
SYMSEM - KIT119, May 1997
please address enquiries to the ESPRIT Information Desk
html version of synopsis by Nick Cook