Towards a Combined Lotos Tool Set


EUCALYPTUS - EC-CAN001

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]


Objectivies and Approach

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).

Progress and Results

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.

Information Dissemination Activities and/or Exploitation

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.


Coordinator

IMAG
avenue Félix Viallet, 46
F - 38031 GRENOBLE Cedex, F

EU Partners

IMAG, F
Université de Liège, B

Non-EU Partners

University of Ottawa (ONT), CAN
Université de Montréal (QUE), CAN
Université de Sherbrooke (QUE), CAN

CONTACT POINT

Prof. Joseph Sifakis
Tel: +33 476 90 96 38
Fax: +33 476 41 36 20
E-mail: Joseph.Sifakis@imag.fr


INCO synopses home page INCO cooperation index INCO keyword index
INCO acronym index INCO number index INCO Projects index
All
synopses home page all keywords index all acronyms index all numbers index

EUCALYPTUS - EC-CAN001, May 1997


please address enquiries to the ESPRIT Information Desk

html version of synopsis by Nick Cook