Protocols, Distributed Systems, Concurrent Systems, Safety Critical Systems, Software Engineering, Specification, Verification, Validation, Testing, Formal Description Techniques, LOTOS, E-LOTOS, Case-studies
Dr. Hubert Garavel
Tel: +33 4 76 61 52 24
Fax: +33 4 76 61 52 52
E-mail: Hubert.Garavel@inria.fr
LOTOS (Language of Temporing Ordering Specification) is a Formal Description Technique for a precise, unambiguous specification of communication protocols and distributed systems. It has been standardized by ISO (International Standard 8807) and applied to the description of large and complex applications.
To be effective, Formal Description Techniques need to be supported by software engineering tools, which allow to execute, simulate, analyze and verify the formal descriptions. During the 80's and early 90's, a number of software engineering tools for LOTOS have been developed. The EUCALYPTUS-1 project has capitalized on this experience and built upon past developments.
At the beginning of the project, several pre-existing tools have been assessed in realistic case-studies, and notably the formal description in LOTOS of the Enhanced Service Transport Protocol (a transport protocol extended with Quality of Service features for multimedia applications) developed in the OSI95 project.
Following this evaluation, several LOTOS tools have been selected and significantly improved. New tools have also been developed. All these tools have been integrated together through a unified graphical user-interface. This has led to a protocol engineering toolset dedicated to the LOTOS language, the EUCALYPTUS Toolset, providing 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 (enumerative, compositional, and on-the-fly) including deadlock and livelock detection, trace analysis, etc.
The EUCALYPTUS tools have 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 many sites (approx. 90) in the world. In June 1994, a special ``EUCALYPTUS day'' intended to industrialists of the telecommunication field was organized in Ottawa.
The EUCALYPTUS-1 participants are taking part into the revision of the LOTOS standard that is currently in progress within ISO. They provided significant contributions, which have been included as annexes in the ISO working documents for Extended-LOTOS.
After December 1994, the EUCALYPTUS-1 has been followed by the EUCALYPTUS-2 project (ISC-CAN-065).
The EUCALYPTUS-2 project is a two-year extension of a previous project, EUCALYPTUS-1 (ESPRIT EC-CA001).
LOTOS (Language of Temporing Ordering Specification) is a Formal Description Technique for a precise, unambiguous specification of communication protocols and distributed systems. It has been standardized by ISO (International Standard 8807) and applied to the description of large and complex applications.
Based upon LOTOS, an advanced protocol engineering toolset during the EUCALYPTUS-1 project. The EUCALYPTUS Toolset provides an extensive set of functionalities: user-friendly extensions of LOTOS datatypes, static analysis, report generation, simulation, generation of C code, graphical display, and formal verification by model-checking (enumerative, compositional, and on-the-fly) including deadlock and livelock detection, trace analysis, etc.
The objectives of EUCALYPTUS-2 are threefold:
During the EUCALYPTUS-2 project, the EUCALYPTUS tools have been used for the design and verification of complex applications and continuously improved. Many successful results have been obtained, some of which can be listed here:
The EUCALYPTUS-2 participants are also taking part into the revision of the LOTOS standard that is currentlty in progress within ISO. They provided significant contributions, which have been included as annexes in the ISO working documents for Extended-LOTOS.
The EUCALYPTUS tools have been demonstrated during international conferences and installed in many sites (currently 125) in the world. The results obtained during the project have been published in scientific journals and international conferences.
Several of the aforementioned case-studies have been performed in close co-operation with Canadian and European industrialists, among which Bull and Bell Northern Research.
Back to the VASY Home Page