The VASY 1999 Roadmap

This year, we are heading in six research directions:

  1. Improvement of compiling techniques for LOTOS

    The long-term effort undertaken in 1998 will come to a successful conclusion. In 1999, we will release new versions of the CAESAR and CAESAR.ADT compilers for LOTOS that will exhibit strong performance improvements in model-checking verification:

    • Significant memory savings in data type implementation
    • Important size reduction of the generated finite-state models
    • Speed increase in execution of the LOTOS programs

    Additionally, we are working to port the LOTOS compilers (as well as the other tools contained in CADP) to the Windows 98 and Windows NT operating systems.

  2. Definition and implementation of Extended-LOTOS

    VASY is actively taking part in the revision of the LOTOS standard undertaken within ISO. This international work is expected to complete in 1999 or 2000 and should produce a new standard named Extended-LOTOS.

    In 1999, we will continue our theoretical work on the definition of Extended LOTOS (Mihaela Sighireanu will defend her doctorate thesis in January 1999).

    In 1999, we intend to release an improved version of the TRAIAN compiler for E-LOTOS. The previous version of TRAIAN released in 1998 offered syntax and static semantics analysis. In addition to bug fixes, the new version will provide code generation for E-LOTOS data types and functions (in the same way as the CAESAR.ADT compiler does for LOTOS).

    As a side effect of the development of the TRAIAN compiler, we have undertaken a reflection on efficient techniques for compiler development. So far, we have used the FNC-2 compiler generator, but we will investigate the use of E-LOTOS as a suitable language for describing and handling abstract syntax trees and attribute computations.

  3. Development of efficient model-checkers

    An important theme of the research done in VASY is the definition and implementation of efficient model-checkers for expressing and verifying correctness properties of concurrent systems involving data.

    In 1999, we will continue to support the XTL 1.1 generic model-checker (distributed a component of CADP). XTL 1.1 is being used in an increasing number of case-studies and derived applications. We namely intend to use it for the verification of robotics controllers.

    Additionally, we will undertake the development of EVALUATOR version 3.0, an on-the-fly model-checker built on top of the OPEN/CAESAR technology. Compared to the existing tool EVALUATOR 2.0, EVALUATOR 3.0 is expected to have a more expressive formula language, a more efficient evaluation algorithm and generate better diagnostics.

  4. Compositional verification

    We will continue our work on the SVL (System Verification Language) language. This language is designed so as to allow a straightforward expression and execution of compositional verification scenarios based on bisimulation and/or model-checking techniques.

    A first version of the SVL compiler already exists; it has been developed using the FNC-2 compiler generator. To overcome the limitations of FNC-2, we plan to improve the SVL compiler by using E-LOTOS as the compiler development language.

    We plan to undertake the development of a tool called BCG_MIN for reducing Labelled Transition Systems according to strong and branching bisimulation.

    Although the first version of BCG_MIN will offer less functionalities than other bisimulation tools (such as ALDEBARAN or FC2TOOLS), the use of the BCG technology (and namely the efficient data structures for storing state and transition tables) should allow BCG_MIN to deal with larger transition systems. Also, in collaboration with the University of Twente, we plan to extend BCG_MIN to stochastic and probabilistic systems.

    The SVL language will be enhanced to support the BCG_MIN tool.

  5. Simulation/debugging for concurrent programs

    In 1998, on request from our industrial partner Bull, we started to design and implement a new simulator to be used both with LOTOS and E-LOTOS. An early version of this simulator, named OCIS (Open/Caesar Interactive Simulator), is already available. Based on (an extended version of) the OPEN/CAESAR interface, OCIS provides advanced features such as: source level code debugging, separate views of concurrent processes, interactive and goal-oriented execution, support for quantitative time, store and load execution scenarios, etc.

    In 1999, this work will be pursued, with the additional goals of porting OCIS to the Windows NT/98 operating system and adapting OCIS to the simulation of UML specifications. Eventually, the resulting tool should become a component of CADP as a replacement for the existing SIMULATOR and XSIMULATOR tools.

  6. Case-studies and industrial applications

    An essential aspect of VASY's approach is the permanent confrontation with real-life problems, mostly issued from industrial needs. Thus, we can pinpoint relevant problems which give matter to new research. In 1999, we will work on the following applications:

    • Validation and test generation for multiprocessor systems, in collaboration with Bull and the PAMPA team of IRISA
    • Validation of smart cards architectures and algorithms, in collaboration with Bull CP8
    • Validation of a SCSI bus arbitration protocol, in collaboration with Bull
    • Validation of two distributed protocols for dynamic reconfiguration of agent-based applications written in Java, in collaboration with the SIRAC team at INRIA Rhone-Alpes

Back to the VASY Home Page