| EUCALYPTUS project | 
|
|---|---|---|
| A European/Canadian LOTOS protocol Toolset |
|
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:
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
|
Editor: - G. Leduc - Webmaster: - RUN Admin - |
Still running IPv4 at: 18.97.9.169... |
RUN |
Montefiore |
ULg © 2000-2025. |