The SENVA Collaboration

SENVA (System ENgineering and VAlidation) is an international joint research gathering the VASY team of INRIA and the SEN2 team of CWI.

Both teams have international expertise as regards the formal specification and computer-aided validation of safety-critical systems (including distributed, embedded, and real-time systems). Both teams share a common methodology based on the theory of process algebras developed by Baeten, Bergstra, Hoare, Milner, and others. Both teams develop (and make available) robust software tools, namely the CADP toolset for VASY (http://cadp.inria.fr) and the mCRL toolset for SEN2 (http://www.cwi.nl/~mcrl), which have been widely used for numerous industrial case-studies.

The SENVA collaboration aims at strengthening a long-standing, although informal, collaboration undertaken several years before 2004. Key objectives for SENVA are to increase the interoperability of the methods and tools developed by VASY and SEN2, and to design the next generation of tools. By joining the competences and workforce of both teams, the intent is to build a world-class leader in formal methods and tools for the safe design of safety-critical systems.

1. Scientific Collaboration between SEN2 and VASY

Before the launch of the SENVA associated team in March 2004, there has been a long-standing history of collaboration between CWI/SEN2 and INRIA/VASY. We recall here the main facts:

Between 1998 and 1999, Radu Mateescu (currently CR1 INRIA at VASY) received an ERCIM fellowship grant and spent 9 months of post-doctoral work at CWI/SEN2.

Software gateways have been established between the mCRL verification tools developed by CWI/SEN2 and the CADP tools developed by INRIA/VASY.

Thanks to these gateways, it has been possible to combine the mCRL and CADP tools to verify several industrial systems. A number of these case studies have been published; see the bibliography below and entries #39, #41, #47, #55, #59, #60, #61, #62, #66, #67, #68, and #69 in the list of case-studies performed using CADP.

In 2003, CWI/SEN2 and INRIA/VASY launched VLTS, the first benchmark suite for explicit state model checking verification. See the International News column in INRIA's Inedit journal Nr. 42 (January 2004) and, for technical details, the VLTS web page.

One key objective of the SENVA team is to provide a formal framework to amplify this collaboration, which so far took place informally.

Joint publications

Wil Janssen, Radu Mateescu, Sjouke Mauw, and Jan Springintveld. Verifying Business Processes using SPIN. Proceedings of the 4th International SPIN Workshop (Paris, France), 1998.

Wil Janssen, Radu Mateescu, Sjouke Mauw, Peter Fennema, and Petra van der Stappen. Model Checking for Managers. Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking (Trento, Italy and Toulouse, France), 1999, LNCS 1680.

Jan Friso Groote and Radu Mateescu. Verification of Temporal Properties of Processes in a Setting with Data. Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology AMAST'98 (Amazonia, Brazil), 1999, LNCS 1548.

2. Scientific Collaborations between INRIA and CWI

INRIA and CWI are two national research institutes in computer science.They have a long-standing tradition of collaboration at the European level, in particular in the ERCIM consortium of which INRIA and CWI are both founding members.

In the past, INRIA and CWI have been involved in several European projects, such as GIPE, CONFER, MADE, and CONFER-2. Currently, INRIA and CWI are partners in four FP6 "networks of excellence", namely Delos, Euro-NGI, Muscle, and Pascal. However, formal collaborations seem to be less present in the last years. For instance, apart from the four aforementioned networks of excellence, we are not aware of any other FP6 action (such as IP, STREP, CA, or SSA) in which both INRIA and CWI would be involved.

Besides SENVA, there is also another associated research team between INRIA and CWI named AirCube dedicated to rewriting techniques. The INRIA project involved in AirCube is the PROTHEO team of Claude Kirchner. The CWI team involved in AirCube is SEN1 - MetaEnvironment, led by Paul Klint.

3. Scientific collaborations between France and The Netherlands

General information about scientific cooperation between France and the Netherlands can be found on the following web-sites: