The VASY 1998 Roadmap

This year, we are heading in six research directions:

  1. 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 1998, we will continue our work on the verification of memory cache consistency protocols for Bull's new multiprocessor architecture PolyKid. This work will focus on the application and evaluation of the TGV-LOTOS tool in order to generate test cases automatically for the Polykid architecture.

  2. Improvement of compiling techniques for LOTOS

    For the aforementioned case-study, we plan to improve the compiling algorithms used in the CAESAR tool. We will focus our efforts on two aspects:

    • A new algorithm for firing epsilon-transitions efficiently
    • Size reduction of the generated finite-state models

  3. Definition and implementation of Extended-LOTOS

    VASY is actively taking part in the revision of the LOTOS standard undertaken within ISO. For 1998, we aim at:

    • Completing the definition of Extended-LOTOS;
    • Continuing the development of our TRAIAN compiler for E-LOTOS undertaken in 1997

  4. Implementation of the XTL model-checker

    An important part of our research is devoted to the definition and implementation of an extended modal mu-calculus for expressing and verifying correctness properties involving data. In 1997, VASY released the XTL 1.1 generic model-checker as a component of CADP 97b "Twente". In 1998, we will undertake the development of XTL 2.0, an improved version allowing extended mu-calculus formulas with value-passing to be evaluated on-the-fly.

  5. Compositional verification

    In cooperation with Laurent Mounier and Jean-Pierre Krimm (Verimag), we will continue our work on compositional verification started in 1997. In 1998, we plan to release the SVL (System Verification Language) language and its associated compiler, which will allow a straightforward expression and execution of compositional verification scenarios.

  6. Simulation/debugging for concurrent programs

    Following the feedback received from our industrial partner Bull, we plan to design and implement a new simulator to be used both with LOTOS and E-LOTOS. This simulator should provide advanced features such as: separate views of concurrent processes, interactive and goal-oriented execution, support for quantitative time, etc.


Back to the VASY Home Page