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:

• In parallel with SENVA, the Technical University of Eindhoven (prof. J. F. Groote) has undertaken work to improve the mCRL language, in particular the "data part", dedicated to the description of data structures, which is based upon abstract data types. A PhD thesis has been started at Eindhoven on this topic; for the moment, this work is disconnected from SENVA and the SPART initiative, and we must find a way to synchronize with this ongoing work in order to reach a consensus on the SPART language.


• Following the departure of the former SEN2 group leader (Wan Fokkink, who became full professor at the Vrije University of Amsterdam) and its replacement by Jaco van de Pol, the research goals of SEN2 are under redefinition before the forthcoming pluriannual evaluation of SEN2.

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:

• Exp.Open was extended to support the composition operators (parallel, hiding, renaming, and cutting) present in the mCRL language, thus enabling the use of compositional and on-the-fly techniques for mCRL specifications.


• Exp.Open was also extended with a partial order reduction technique, which allows to reduce the number of states to explore during verification, while preserving branching bisimulation. This technique allows to reduce the state space of some specifications by several orders of magnitude.


• An interface for a process P in a system of communicating processes S is an automaton that models partially the environment of P within S. Using the Projector tool of CADP, this interface allows to reduce (often significantly) the number of states and transitions of P that must be explored during the state space enumeration of S. In the framework of communicating processes connected using LOTOS operators, every automaton corresponding to a process in the environment of P can be used as interface. However, this is not anymore true when processes are connected using mCRL operators. In 2004, Exp.Open was extended to generate interfaces automatically for systems of communicating processes connected using any of the operators implemented in Exp.Open, including mCRL ones. This functionality thus allows to use Projector in the framework of mCRL.


• In order to apply the on-the-fly verification tools of CADP to mCRL descriptions, a new tool called mcrl.open was developed. This tool translates mCRL descriptions into their corresponding transition systems, represented implicitly (i.e., by means of their successor function) according to the OPEN/CAESAR generic API. Two different schemes for representing states of mCRL descriptions were studied, leading to two successive versions of mcrl.open.


• Discussions with Jaco van de Pol allowed to improve CADP tools in several ways. In particular, Exp.Open and the hide_1 and rename_1 OPEN/CAESAR libraries for label handling were modified to support labels corresponding to mCRL actions. In this way, all OPEN/CAESAR tools for on-the-fly verification, including Projector, can now be used on mCRL descriptions.

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:

• While SEN2 builds its tools on top of MPI, VASY develops a dedicated communication library implemented using UNIX sockets, which allows a fine tuning of the performance for particular needs. Discussing the idea of providing an alternative implementation of this communication library using MPI, showed that subtle differences in the communication protocols made this idea a non-trivial task.


• CWI/SEN2 and INRIA/VASY used different, incompatible file formats to store their distributed transition systems: VASY is using N files with reversed transitions, whereas SEN2 uses 3N+2 files with direct transitions. As a solution for the latter problem, SENVA defined a new common file format, named "PBG 1.0" (Partitioned BCG Graph), which is used by the latest versions of the distributed verification tools. Stefan Blom already developed conversion tools between the file format previously used by SEN2 and PBG 1.0.

5. Other aspects

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

• The installation of the CADP and mCRL tools on VASY and SEN2 computing platforms, which use different operating systems, allowed to identify and correct several problems:
  
  
  1. The mCRL toolset did not install correctly on the machines of VASY, which are running under Solaris.
  
  
  2. The mCRL prover did not compile and detected the host machine architecture erroneously.
  
  
  3. Two problems of the Installator tool of CADP when executed on a laptop computer were corrected.
  
  
  4. An erroneous double initialisation of the OPEN/CAESAR libraries was corrected in the OCIS simulator of CADP.
  
  
  5. A variable naming causing a clash with other identifiers in the mCRL libraries was corrected in the EVALUATOR tool of CADP.


• Every year, INRIA/VASY holds a 3-4 day scientific seminar (near Grenoble) in which the work done and future perspectives are discussed. As a side comment, the practice of such seminars was highly praised by the external reviewers of the former 1C theme of INRIA (March 2003), who recommended that other INRIA teams should do the same.
   
  In 2004, we extended this event by inviting all SENVA participants to a joint 4-day scientific seminar, which took place in Allevard-Les-Bains (near Grenoble) from June 21 to June 24. This seminar, held in English, was the occasion to discuss work done and future perspectives. Besides INRIA and CWI teams, two invited researchers attended the seminar, namely Judi Romijn (Technical University of Eindhoven) and Holger Hermanns (University of Saarbruecken). The program of the seminar is available on the web at http://vasy.inria.fr/senva/workshop2004.


• Three other meetings between SENVA members were held at the occasion of various scientific events:
  
  
  1. The ETAPS’2004 European Joint Conferences on Theory and Practice of Software (Barcelona, Spain), March 27 – April 4, 2004 (SENVA participants: Wan Fokkink and Hubert Garavel).
  
  
  2. The AMAST’2004 International Conference on Algebraic Methodology and Software Technology (Stirling, Scotland), July 12-16, 2004 (SENVA participants: Jaco van de Pol, Jun Pang, and Wendelin Serwe).
  
  
  3. The seminar of FMICS, the ERCIM Working Group on Formal Methods for Industrial Critical Systems (Aix-les-Bains, France), April 20-22, 2004 (SENVA participants: Jaco van de Pol, Wan Fokkink, Hubert Garavel, and Radu Mateescu).


• Several collaborations were started with external partners, both from The Netherlands and France:
  
  
  1. Prof. Judi Romijn (Technical University of Eindhoven) uses both mCRL and CADP tools and therefore is particularly well positioned for evaluating the results of SENVA. Prof. Romijn has already applied these results to significant communication protocols, such as the panic recovery protocol of the international standard IEEE 1394.
      
     In 2004, several versions of the panic recovery protocol were specified in LOTOS and analysed using the CADP tools. Two deadlocks were found by VASY in a non-trivial configuration of the protocol, consisting of two processes and involving two changes in the network topology. After these deadlocks were reported to Eindhoven and corrected, another one was discovered together by VASY and SEN2: the CADP compositional verification tools were used to generate a state space of about 1.7 GBytes (500 million transitions), which was subsequently minimized using the BSIM2 tool of SEN2.
  
  
  2. We also expect collaborations with other INRIA projects:
     
     
     • The OASIS project, in the context of FIACRE, a cooperative research action (ACI) on the safety of distributed components assembly, funded by the French ministry of research.
     
     
     • The APACHE and GRAAL projects, which are working on grid computing and can offer high-performance platforms for benchmarking distributed verification tools.

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. http://www.ercim.org/publication/Ercim_News/enw58/fokkink.html