Scientific Goals

Created in January 2000 as an official INRIA project, VASY participates in the international effort to produce reliable systems by using formal methods. The intended application domain is broad, encompassing hardware, software, and telecommunication systems.

VASY promotes the use of formal description techniques supported by software engineering tools. The formal description effort is rewarded by the ability to perform rapid prototyping, simulation, partial or exhaustive verification, and to generate test suites automatically.

VASY's aim is to deliver industrial-strength methods and software tools that enable early error detection and increase confidence in the systems under design. In particular, VASY contributes actively to the development of the well-known CADP protocol engineering toolbox.

VASY is involved in three research directions:

Languages and compilation

This aspect of VASY research deals with formal specification languages for describing concurrent systems. Such languages are important to users because they constitute the entry point of the formal design process. Among all possible languages, VASY focuses on those with a rigorous semantics and appropriate compositional properties.

  • Process algebras are considered because of their expressiveness and strong theoretical foundations. In particular, VASY develops compilers for LOTOS, a process algebra standardized by ISO (International Standard 8807) that combines the best features of Milner's CCS and Hoare's CSP calculi. LOTOS is used in many case-studies at INRIA and around the world, and VASY is working to optimize the LOTOS compilers and to extend them for rapid prototyping and testing purposes.

  • In addition to classical process algebras, VASY also explores new specification languages (such as E-LOTOS and LOTOS NT), which are designed to gain better acceptance in industry. These languages combine features of process algebra (for the description of concurrency) with features of functional and imperative languages (for the description of data types and sequential computations). VASY contributes to the definition, study, and implementation of E-LOTOS and LOTOS NT, notably with the TRAIAN compiler and the NTIF model and tools for symbolic transition systems.

        More information...

Models and verification

Research into models and verification deals with the validation and verification of concurrent systems. We pursue three main goals:

  • Enhancing temporal logics and verification tools

    Typical temporal logics enable specification of system correctness properties, but suffer from an important limitation regarding properties that involve data. To address this limitation, VASY has extended the mu-calculus with high-level constructs to reference the typed data contained in messages exchanged between distributed system components. The next step is to efficiently compile and verify properties of the mu-calculus containing data (EVALUATOR 4.0 and XTL model checkers, CAESAR_SOLVE library).

  • Fighting state explosion

    A key issue in enumerative verification is the combinatorial explosion in the number of states. To cope with state explosion, we consider in particular three directions:

    • Symbolic analysis techniques, which analyse the data flow of functions and processes.

    • Compositional verification, which separately (as far as possible) processes the sequential components of a parallel system under verification. The efficiency of this approach can be improved by combining it with techniques based on partial orders and the detection of symmetries. CADP includes several verification tools to make compositional verification more efficient and more automated (SVL language and compiler, PROJECTOR and EXP.OPEN tools, etc.).

    • Massively parallel verification, which exploits the resources (such as memory and CPU time) provided by the parallel and distributed architectures, in particular clusters of PCs. Our objective is to develop new CADP verification tools to handle systems with billions of explicit states (DISTRIBUTOR and BCG_MERGE tools).

  • Designing generic components for verification, test, and performance evaluation

    For a number of years, we have been delivering our research results in the form of software components, which can be used to build tools of increasing sophistication. Several research teams around the world are applying the generic technologies developed by VASY to languages other than process algebras. These include B, Petri Nets, SDL, UML, as well as probabilistic, stochastic, and timed systems. The components delivered by VASY feature:

    • Efficient handling of very large explicit Labelled Transition Systems (BCG format and associated tools)

    • Efficient computation of strong and branching bisimulation for non-deterministic, probabilistic, and stochastic transition systems (BCG_MIN tool)

    • Language-independent representation of implicit Labelled Transition Systems (OPEN/CAESAR environment and associated tools)

    • Software tools that bring the domains of formal verification and performance evaluation nearer to each other (BCG_STEADY, BCG_TRANSIENT, and DETERMINATOR tools)

    • Efficient on-the-fly resolution of boolean equation systems with diagnostic generation, which are likely to serve in verification based on mu-calculus and bisimulations, and perhaps also in test generation, partial-order verification, and controller synthesis (CAESAR_SOLVE library)

        More information...

Case-studies and industrial applications

In order to demonstrate the applicability of our methods and tools to real-life applications, we have established academic and industrial partnerships.

        More information...

Version 3.11 - Date 2015/09/09 12:09:29

Back to the VASY Home Page