Keywords: protocols, distributed systems, concurrent systems, specification, LOTOS, verification, formal description techniques, safety critical systems, E-LOTOS
Start Date: 1 November 93 / Status: finished / Duration: 24 months
[ participants / contact]
LOTOS is a formal description technique for a precise, unambiguous specification of communication protocols and distributed systems. It has been standarised by ISO 8807 and applied to the description of large and complex applications. In order to be effective, formal description techniques need to be supported by software engineering tools which allow to execute, simulate, analyse and verify the formal descriptions. During the 80's and early 90's, a number of tools for LOTOS have been developed. The project builds upon this experience and will help define a framework for the integration of Lotos academic prototype tools for the specification of concurrent and distributed systems.
European links: ESPRIT BRA REACT (6021) and CONCUR-2 (7166), project 5341 (OSI95), COST-247, EUCALYPTUS-2 (EC-CAN65).
At the beginning of the project, several pre-existing tools have been assessed in realistic case studies, and notably the LOTOS formal description of the Enhanced Service Transport Protocol, a transport protocol extended with quality of service features for multimedia applications, that was developed in the OSI95 project. Following this evaluation, several LOTOS tools have been selected and significantly improved and new tools have been developed. All these tools have been integrated through a unified graphical user-interface. This has led to a LOTOS protocol engineering tool set, the EUCALYPTUS Tool Set, which provides an extensive set of functionalities: user-friendly extensions of LOTOS data types, static analysis, report generation, simulation, generation of C code, graphical display, and formal verification by model-checking including deadlock and livelock detection.
The EUCALYPTUS tools have been assessed on large case studies including the OSI95 transport service, telephony systems and avionic systems. They have been demonstrated during international conferences and installed in approx. 90 sites in the world. A special "EUCALYPTUS Day" for industrialists in the telecommunication area was organised in Ottawa in 1994.
The EUCALYPTUS participants take part into the revision of the LOTOS standard that is currently in progress.
Further information is available from the project home page: http://www.inrialpes.fr/vasy/pub/eucalyptus.html.
avenue Félix Viallet, 46
F - 38031 GRENOBLE Cedex, F
Université de Liège, B
University of Ottawa (ONT), CAN
Université de Montréal (QUE), CAN
Université de Sherbrooke (QUE), CAN
Prof. Joseph Sifakis
Tel: +33 476 90 96 38
Fax: +33 476 41 36 20
EUCALYPTUS - EC-CAN001, May 1997
please address enquiries to the ESPRIT Information Desk
html version of synopsis by Nick Cook