EUCALYPTUS project @ RUN
ULg EUCALYPTUS project RUN
A European/Canadian LOTOS protocol Toolset


Home

People

Research Topics

Projects

Publications

IFIP WG 6.1

Events and Conferences

CSS

How to Reach Us

EUCALYPTUS stands for "European/Canadian LOTOS Protocol Tool Set. It is a European/Canadian project whose objective is the development of an integrated toolset for the LOTOS language.

The project was launched in January 1993 for two years (ECCA 001:76099) and has been extended (ISC-CAN-65) for two more years until December 1996.

On the European side, the project is funded by the European Commission (DG III).

It involves the following partners:

  • Verimag, Grenoble, France (Prof. J. Sifakis, Dr. Hubert Garavel), main contractor.
  • University of Liège, Belgium (Prof. A. Danthine, Dr. Guy Leduc)
  • University of Ottawa, Canada (Prof. L. Logrippo)
  • University of Montreal, Canada (Prof. G.v. Bochmann)
The EUCALYPTUS toolset consists of several tools developed by the partners and integrated in a unified user-friendly interface, jointly developed by the partners.

The main tool functions are the following:

Support of LOTOS extensions: It is possible to use compact user-friendly notations to specify the datatypes and then use a preprocessor to expand them into standard LOTOS. The tools are called APERO and have been developed at the University of Liège. These tools are now available

Static analysis: The LOTOS specifications can be checked by the lexical, syntactic and static semantic analyzers.

Report generation: The LOTOS descriptions can be pretty-printed and cross-references generated.

Simulation: It is possible to execute the LOTOS specification in several modes: interactive (step by step with backtracking), symbolic expansion (in which input values are handles symbolically), goal-oriented (in which a given action in searched for) and ramdom. These functions are part of the ELUDO toolset developed at the University of Ottawa.

Model generation: It is possible to generate the Labelled Transition System (LTS) associated with the LOTOS description. The tools are called CÆSAR and CÆSAR.ADT and are part of the CADP toolset developed in Verimag. This LTS model can then be verified by other tools.

Model verification: An LTS model can be verified in several ways. It can be minimized and compared modulo various equivalences (e.g. strong bisimulation, observational, branching bisimulation, delay and safety) and preorders (e.g. strong simulation and safety). A diagnostic sequence is provided when the model is incorrect. The tool is called ALDEBARAN and is part of the CADP toolset developed in Verimag.

Compositional and on-the-fly verifications: When state explosion occurs in the generation of the LTS, several alternative verification methods are available, such as the compositional verification and the on-the-fly verification. These functions are part of the CADP toolset developed in Verimag.

Other verification features: Deadlock and livelock detection, search of specific execution sequences, model-checking of mu-calculus formulas. This open toolbox called OPEN/CAESAR is part of the CADP toolset developed in Verimag.

Model display: The generated or minimized LTS models can be displayed graphically (i.e. in postscript) and edited. These BCG_Draw and BCG_Edit tools are part of the CADP toolset developed in Verimag. Another tool, called VISCOPE and developed at IRISA (Rennes), is also integrated and allows 3D visualization of graphs.

C-code generation: From LOTOS descriptions, one can produce C code to be interfaced and used in application programs. These functions are part of the CADP toolset developed in Verimag.

Trace analysis: It is possible to verify whether a given trace (ecesution sequence) can be obtained from a LOTOS description. This allows the validation of test suites and their verdicts with respect to a LOTOS description representing the system under test. This tool is called TETRA and has been developed at the University of Montreal.

Test generation: It is possible to generate test sequences from the LTS model. This function is part of the tool TESTGEN-LOTOS developed at INT (Paris).

Publications

* VLib: Infinite virtual libraries for LOTOS
C. Pecheur
Keywords : languages constructs and features, processors, programming languages
Read the abstract
Download the PostScript document or the compressed PostScript (gzip) document
Proc. of the IFIP TC6/WG6.1 Thirteenth International Symposium on Protocol Specification, Testing and Verification, 25-28 May 1993, Liège, Belgium, A. Danthine, G. Leduc, P. Wolper (eds.), Protocol Specification, Testing and Verification XIII, pp. 29-44, Elsevier Science

[ Home | People | Research Topics | Projects | Publications | IFIP WG 6.1 | Events and Conferences | CSS | How to Reach Us ]

Editor: - G. Leduc -
Webmaster: - C. Soldani -
Still running IPv4 at: 3.81.30.41... RUN | Montefiore | ULg
© 2000-2024.