SENVA Scientific Report 2004

Both CWI/SEN2 and INRIA/VASY are conducting research on the formal specification and computer-aided verification of safety-critical systems. They share a common approach based on the established theory of process algebra. However, a distinctive mark of their work is the particular effort to create a bridge between theory and applications, especially by developing robust software tools (the CADP and mCRL toolsets) and assessing the capabilities of their tools on complex, industrial case-studies. The goal of SENVA is to join and coordinate workforces in order to ensure a stronger impact at the European and world levels.

In 2004, we explored four scientific directions.

1. High-level specification languages

By now, the CADP and mCRL toolsets use similar, but incompatible input languages. CADP supports LOTOS (an ISO standard for the specification of telecommunication protocols) while mCRL supports the mCRL language (a formalism widely used in The Netherlands). A suitable goal is to reach consensus on a common formalism, the "SPART language" (Standard Process Algebra Research & Tools), that would ultimately replace both LOTOS and mCRL. Taking into account that LOTOS and mCRL are relatively old languages (designed in 1989 and 1993, respectively), the SPART language should benefit from the latest advances in terms of formal methods and language semantics. Also, the SPART language should be suitable for both theorem proving (in which CWI/SEN2 has a strong expertise) and enumerative verification (which is the core of research done at INRIA/VASY).

In 2004, we built a dedicated Web site which contents management features to hold the discussion on the definition of the SPART language. Three electronic, web-based questionnaires have been activated in order to start a structured discussion, involving not only members of SENVA, but also of the "Universitaet des Saarlandes" (Saarbruecken, Germany) and LAAS-CNRS (Toulouse, France). These questionnaires focus on the causes of the "crisis" of process algebra and the goals, risks, and expected benefits of the SPART initiative.

Six thematic forums have been spawned off in order to enable a more interactive discussion of some particular technical points, such as the description language for data (abstract data types vs. functional languages, iteration vs. recursion, priorities, etc.) or real-time. After voting, all participants agreed on the goals and usefulness of the SPART approach.

However, in 2004 the situation has evolved considerably due to new facts:

Due to these events, the work undertaken by SENVA on SPART has been suspended until it will become clearer whether it fits or not in the new research strategy that will be adopted by SEN2.

2. Minimization tools for transition systems

During the past years, CWI/SEN2 and INRIA/VASY have developed competing tools (BCG_MIN and BSIM2) for equivalence checking, a mainstream verification technique based on the concept of bisimulation between transition systems (which represent state spaces). Both tools use different algorithms and exhibit good performances on large examples. However, depending on the examples, it happens that one tool is more efficient than the other, and vice-versa. Therefore, it would be suitable to study the performances of both approaches and, if possible, try to integrate both tools into a unique one that would always deliver the best performances.

In 2004, we have undertaken a careful study of BCG_MIN and BSIM2 performances by using the VLTS benchmark suite that we developed in 2003. The results of this study indicate that each of the BCG_MIN and BSIM2 tools exhibits better performances than the other on certain transition systems. Therefore, both tools keep their practical interest and therefore should be kept separate. To make both tools available to users in a uniform manner, the interfacing of LTSMIN (the new version of BSIM2) with the CADP tools has been undertaken.

Also, the process of thoroughly testing and benchmarking the tools allowed to spot and correct a problem in the BCG_MIN implementation of the stochastic branching bisimulation algorithm.

3. Compositional verification techniques

A central problem in computer-aided verification of safety-critical systems is state explosion, which is caused by the following fact: A linear growth in the size of the source-level code often causes an exponential growth of the corresponding transition system that represents all reachable states of the system. SENVA focuses on methods and tools to face state explosion. In particular, we are joining forces to implement efficient techniques such as partial orders (including the so-called tau-confluence reductions) and compositional verification.

In 2004, a significant part of the SENVA collaboration was devoted to the Exp.Open tool of CADP, which was enhanced in several complementary ways:

4. Distributed algorithms for state space generation

Another way to attack state explosion consists in using many computers instead of a single one. Of particular interest are recent machines for distributed and massively parallel computations, especially clusters of PCs. Both CWI/SEN2 and INRIA/VASY have ongoing research in this direction and have developed prototype tools (which have not yet been released outside). One goal of SENVA is to determine synergies between these activities in order to push forward the limits of verification.

The meetings between SENVA partners were used for discussing the teams activities in distributed and massively parallel verification, including demonstrations of the existing tools. During his visit to VASY, Stefan Blom also successfully installed his distributed tools on the cluster of INRIA's APACHE project used by VASY. In the discussions, several differences in the approaches became apparent:

5. Other aspects

Besides the work undertaken along the main scientific directions described above, we carried out several other activities during 2004:

Joint publication

Wan Fokkink, Hubert Garavel, and Jaco van de Pol. CWI and INRIA join Forces on Safety-Critical Systems. ERCIM News #58, July 2004.