In 2006, we explored four scientific directions.
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.
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.
Other advances have been made by both SENVA partners regarding the combination of different verification techniques, namely:
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.
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.