|
|
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 2005, we explored four scientific directions.
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.
A first application of the CADP and mCRL tools to a fair payment protocol was done at SEN2 by Muhammad Torabi Dashti in 2004, who modelled this protocol using an extension of the Dolev-Yao model with fair channels and verified 12 security properties (correctness, effectiveness, timeliness) written in alternation-free mu-calculus.
During the first year of the SENVA collaboration, a significant effort was poured into tools for compositional verification, most notably the Exp.Open 2.0, Projector 2.0, and SVL tools of CADP, and the “mcrl.open” tool of the mCRL toolset (see the SENVA 2004 scientific report for details).
In 2005, in order to evaluate the outcome of these recent tool improvements, the SENVA team has been applying these tools to security protocols for e-commerce under study at CWI. So far, the technical results are the following:
To proceed for more complicated case studies, several directions have been investigated by the SENVA team:
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.
The work undertaken by SENVA in 2004 was fruitful in bringing 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. VASY modified its tools in order to use this new format and Stefan Blom (CWI) developed conversion tools between PBG 1.0 and the file format previously used by SEN2 tools.
In 2005, this work was temporarily slowed after the PhD defense of Simona Orzan (who left SEN2 in June 2004, but keeps a guest position at CWI one day a week) and the departure of Stefan Blom (who left SEN2 to the University of Insbruck in January 2005). However, we expect to maintain an active collaboration with them, especially in the framework of SENVA meetings (both Stefan Bloam and Simona Orzan will participate to the forthcoming SENVA meeting on November 16-17).
VASY took advantage of this pause to finalize a “clean” version of its Distributor and Bcg_Merge tools for massively parallel verifications. In 2005, these tools have been integrated into CADP as official components and distributed to a number of partners. For instance, Judi Romijn and her students at Technical University of Eindhoven use both mCRL and CADP tools to verify significant communication protocols, such as the panic recovery protocol of the international standard IEEE 1394. Using the massively parallel tools, they managed to analyze non-trivial configurations of this protocol and detect several problems.
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).
Another promising direction for collaboration is automated generation of test cases from high-level formal specifications of reactive systems with data.
At CWI, in the framework of the TT-Medal project, Jens Calame (PhD student) and Natalia Ioustinova (postdoc researcher) are using TGV 2.0 (Test Generation based on Verification), a software tool developed at INRIA Rennes and integrated in the CADP verification toolbox. More precisely, they are using abstraction (to get a finite-state system from an infinite one), then TGV (to get abstract test cases), then constraint solving (to get concrete test cases from abstract ones), and finally translate concrete test cases into the TTCN-3 language.
One important issue for TGV (and also for verification in general) is combinatorial complexity leading to state-space explosion. Christophe Joubert and Radu Mateescu are addressing this issue by developing a parallel version of TGV that can work on networks of workstations and clusters of PC.
The development of interoperable software tools is a key aspect of the SENVA collaboration. In 2005, the development of the CADP and mCRL tools continued. In particular, the visits organized during the SENVA collaboration allowed to identify and fix several issues in the Exp.Open 2.0 tool of CADP (which was developed during the first year of the SENVA collaboration), when this tool was used in conjunction with the mCRL tool set.
The SENVA team is actively contributing the “Handbook of Formal Methods” (to appear in 2006) coordinated by Stefania Gnesi. This handbook will include chapters written by Wan Fokkink (SEN2) and Radu Mateescu (VASY).