CWI INRIA

SENVA Scientific Report 2006

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 2006, we explored four scientific directions.

1. Distributed algorithms for state space generation and minimization

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 tools. One goal of SENVA is to create synergies in this area so as to push forward the limits of verification.

In 2004, to bring the SEN2 and VASY tools closer, 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.

In 2005, CWI managed to obtain Dutch funding to pursue the SENVA goals in massively parallel verification. Precisely, SEN2 obtained a Dutch grant on this topic, together with the Universities of Eindhoven and Twente (VeriGEM project).

In 2006, VASY has enhanced massively parallel verification tools, by enhancing the CAESAR_SOLVE_2 library and developing new tools (PBG_CP, PBG_MV, PBG_OPEN, PBG_RM) supporting the PBG format. SEN2 has been refined the graphical interfaces and studying checkpointing and beam search concepts.

2. Application of model checking to bio-informatics

During the SENVA meeting on clusters and grids for verification and performance evaluation (November 15-16, 2005), intensive discussions took place on building a European project. These discussions continued in 2006 and led to a project proposal named EC-MOAN that was approved by the European Commission and should start on January 1st, 2007.

The aim of EC-MOAN is to enhance our understanding of the molecular mechanisms underlying the behavior of complex living systems. In particular, it will investigate how large and complex regulatory networks control the response of a living cell to its ever-changing environment. The stress response to environmental events is induced by the interaction of several interwoven modules with complex dynamic behavior, acting on different time scales. To deal with this complexity mathematical modeling and computer-supported analysis are needed. So far, the methods of systems biology are mostly applied to individual modules, such as particular metabolic pathways and genetic networks. But to understand the global behavior, an integrated description of the regulatory network is required, as well as new, scalable methods for modeling and analyzing integrated networks.

EC-MOAN will develop an integrated model for the stress response system of the entero-bacterium Escherichia coli (one of the best studied organisms and a model for several pathogenic bacteria), including key metabolic, genetic and signaling modules. It will also develop methods to reduce high-dimensional nonlinear systems of equations, and to approximate them by discrete automata. Parallel model checking algorithms will be developed for verifying specific properties at the model. This will allow to explore the models and predict the outcome of experiments. This should give a coherent and generic methodology, generalizable to other complex (biological) systems, thus improving many medical and biotechnological applications, e.g. strain improvement and rational drug design.

The EC-MOAN project gathers a cross-disciplinary European team of biologists, mathematicians, and computer scientists. It is led by Dr. Jaco van de Pol (SEN2 team of CWI and SENVA co-chair). INRIA Rhône-Alpes (VASY and HELIX team) will play a major role in EC-MOAN as well.

3. Software development

The development of interoperable software tools is a key aspect of the SENVA collaboration. In 2006, the development of the CADP and mCRL tools continued. In particular, the Mcrl.Open tool of CWI was adapted to be compatible with CADP 2006, the stable release of CADP to be issued in December 2006.

Other advances have been made by both SENVA partners regarding the combination of different verification techniques, namely:

4. Common case-studies

SENVA collaboration also took place around common case-studies. In particular, we can mention the study of an embedded controller for a unit dedicated to the drilling of metallic products. This case-study is a significant example of an industrially critical system, the embedded controller being sufficiently simple to allow a relatively compact formal description, and sufficiently complex (it consists of several parallel components communicating asynchronously) to require formal analysis.

The SEN2 team participated to the formal specification of the drilling unit using several languages (Chi, mCRL, Promela, and timed automata) and to its analysis by means of the associated tools (mCRL, CADP, SPIN, and UPPAAL). A paper on this subject was published in 2004 by Bortnik, Trcka, Wijs et al.

In 2006, Radu Mateescu (VASY) formally specified in LOTOS two versions of the controller (a sequential and a distributed version). A set of safety and liveness properties characterizing its correct behaviour was formulated using regular alternation-free mu-calculus. The corresponding files are available from here. Using the BISIMULATOR and EVALUATOR 3.5 tools of CADP, the compatibility between these two versions was established, and the correctness of the controller with respect to the temporal properties was proven. This case-study led to a tutorial publication.

5. Joint meetings

In April 2006, SENVA organized at CWI the second edition of a dedicated workshop gathering most European experts on massively parallel methods for verification and performance evaluation. The first edition of this SENVA workshop took place at INRIA Rhône-Alpes in November 2005. The scientific programme and the presentations given at the second edition of this workshop are available at http://vasy.inria.fr/senva/meeting2006.

Every year, SENVA holds a plenary scientific seminar in which the work done and future perspectives are reviewed. In 2006, this seminar took place in Venosc (near Grenoble) during three days (June12-14). This seminar was the occasion to discuss work done and future perspectives. Besides INRIA and CWI teams, four invited researchers attended the seminar, namely Rodolfo Gomez and Li Su (University of Kent at Canterbury), Manuel Baclet (ENSEEIHT), and Sylvain Peyronnet (EPITA, now LIX). The detailed program of the seminar is available on the web at http://vasy.inria.fr/senva/workshop2006.

In addition, regular meetings between SENVA members were held at the occasion of various scientific events and mutual visits.

Finally, the achievements of the SENVA team have been presented during an evaluation meeting held on November 28, 2006 at INRIA Rocquencourt (France). The slides presented by Jaco van de Pol and Hubert Garavel during this meeting can be found here.

Joint publications

The SENVA team is actively contributing the Handbook of Formal Methods (to appear in 2007) coordinated by Stefania Gnesi. This handbook will include chapters written by Wan Fokkink (SEN2) and Radu Mateescu (VASY), the latter being devoted to the aforementioned embedded controller for the drilling of metallic products.