Evaluation Report on INRIA INRIA Research Theme ComC (excerpt)

June 2007

Vasy

The evaluation of VASY was performed by the following panel members:

1. Project Profile

The VASY project focuses on the development and application of automated formal-modeling and verification tools for asynchronous concurrent systems. The orientation toward asynchrony distinguishes the project technically from the other ComC projects, which are generally devoted to the modeling and analysis of synchronous systems. VASY was officially established in January 2000 and is based in INRIA Rhône-Alpes, with a small satellite group in Dijon.

The specific activities of the team are centered around the CADP verification tool suite and include research into new verification techniques, methodologies for applying automated verification, and applications to problems in the area of embedded systems, hardware design and, recently, systems biology. CADP is distributed publicly and has a significant international user community.

2. Evaluation of Activities 2003-2007

The evaluation of the VASY activities during the period of performance is based on the criteria distributed to the evaluation team. These include: scientific excellence; adequacy to INRIA’s scientific strategy; industrial transfer and partnerships; and manpower and means. The rest of this section considers each of the points in turn.

2.a. Scientific excellence

The project’s staff was very active scientifically during the evaluation period, publishing 36 peer-reviewed papers while maintaining and issuing new releases of the CADP tool suite. The venues in which the papers were published are among the best in the international formal-methods community, and include conferences such as Computer-Aided Verification (CAV) and Tools and Algorithms for the Construction and Analysis of Systems (TACAS), and journals such as Theoretical Computer Science and Science of Computer Programming. The results obtained by the project team were devoted to improved techniques for automated verification, and case studies involving the use of CADP, and thus were highly coherent with the project’s technical goals. Specific achievements include: The first and last results are also noteworthy for reasons beyond their scientific and engineering ingenuity. VASY emphasizes two aspects in its verification activities: so-called model-based analysis, which is in line with other automated verification groups around the world; and language-based analysis, which uses ideas from programming-languages to improve verification. This combination of emphases is distinctive of the VASY approach and yields highly attractive results. It should also be noted that the last item represents a convincing riposte to one of the concerns raised in the 2003 evaluation report: that the team is too invested in LOTOS, a niche modeling language. That LOTOS may be used as an intermediate language to support other languages in CADP is good justification for continued enhancement of LOTOS support.

VASY personnel had high profiles in the scientific community during the evaluation period; team members served on program committees of a number of international technical conferences. The project lead (Garavel) also chaired the program committee for TACAS, served on the steering committee for two years of an international workshop series on parallelization of formal-methods tools, and edited a special issue of the journal Software Tools for Technology Transfer.

Based on these observations, it is apparent that the project is very productive scientifically and has strong visibility in the international research community. The scientific topics being studied are also coherent with the technical topic of the project.

2.b. Alignment with INRIA’s scientific strategy

VASY’s focus on formal methods for asynchronous systems dovetails well with INRIA’s over-all strategy. The project serves two of INRIA’s research themes very well: embedded systems (several embedded case studies have been undertaken by the team and others using the CADP verification tools), and formal methods.

2.c. Industrial transfer and partnerships

VASY participated in several significant industrial partnerships and projects. Three studies stand out: the ongoing collaboration with Bull on the use of CADP to verify cache-coherency protocols; a project with personnel at the Commissariat à l'Énergie Atomique (CEA) on asynchronous hardware design; and a newly launched initiative on the use of CADP in biological-system modeling undertaken in conjunction with the Helix team in Grenoble. While Helix is not an industrial team, its Genetic Network Analyzer (GNA) tool is distributed commercially, and the VASY team has collaborated with Helix to enhance GNA with an interface to CADP. VASY also maintains ongoing interactions with STMicroelectronics and Airbus through the Topcased and Multival projects.

2.d. Manpower and means

The VASY team has grown significantly since the last evaluation. The growth is in line with the expansion of the projects activities. The team has taken steps to address a minor shortcoming in its personnel portfolio - the lack of student involvement in the project - by formalizing a connection with the Grenoble Universities’ LIG laboratory. Three new PhD students at the lab have also been hired directly by Bull, INRIA and STMicroelectronics.

3. Evaluation of Proposed Activities after 2007

The VASY team cites technology transfer as the primary motivation for their proposed efforts over the next four years. For a mature project (VASY has been operational as a project since 2000) with a heavy emphasis on technology development, this motivation is appropriate. The group rightly notes that both asynchrony and modeling pervade hardware and software design; thus, the team’s continued focus on formal methods for asynchronous systems is also well considered. The rest of this section analyzes the teams proposed directions using the evaluation criteria cited previously.

3.a. Scientific excellence

The proposed research directions can be categorized along two axes. The first involves continued enhancements to the core CADP tool suite, at both the algorithmic and language-processing level. These results are likely to yield incremental advances in verification-tool engineering that will improve CADP while being primarily of interest to tool engineers. One departure from this general trend is the team’s new emphasis on the combination of model checking and performance evaluation. This new addition to CADP functionality will further position the tool as a system-engineering tool. It should be noted that VASY has attracted one Prof. Holger Hermanns, one of the pre-eminent researchers world-wide in this field, to work with them on this effort.

The second scientific direction involves novel applications of CADP technology, and the anticipated results are likely to be quite interesting. The bio-informatics work in particular represents a quite novel direction for the team. This might be a concern in general (does the team have the right personnel?), but there are already promising early results in the area. The anticipated collaboration with industrial and governmental partners in avionics and hardware design will play a significant role in helping to transition CADP technology outside of the research laboratory.

3.b. Alignment with INRIA’s scientific strategy

As noted in the previous section, the VASY team’s profile fits quite naturally into INRIA’s scientific strategy.

3.c. Industrial transfer and partnerships

As noted above, the team mentions technology transfer as a main motivation for its activities during the coming years. Its case-study work with current partners will provide a measure of support for this, and its involvement with two pôles de compétitivité will give the team visibility to other potential partners and industrial users. The team is encouraged to develop a strategy for exploiting these relationships, and also to begin developing a plan for exploring possible commercialization strategies for CADP.

3.d. Manpower and means

The team has a measured strategy for growth in the coming years that is consistent with the growth of its activities. The development of a satellite group in Dijon is likely to present some management challenges that the team is encouraged to prepare for.

4. Conclusions and Recommendations

The VASY team has made remarkable scientific and technology-transfer strides during the evaluation period. The group has maintained a consistent focus on formal methods for asynchronous systems, and its depth in both model-based and language-based analysis has enabled it to make high quality scientific contributions on the international stage. The VASY team members and management are to be congratulated on maintaining a distinctive focus while also maintaining a level of flexibility on the research to be pursued.

The evaluation team has two recommendations for the coming term of the VASY project.

  1. The development and growth of a satellite office in Dijon is likely introduce management and administrative challenges. Provided this has not already been done, the team is encouraged to develop a plan for addressing these.

  2. The VASY project is maturing, and team members are encouraged to develop plans for ensuring the continued distribution of its technology, either via commercialization or some other means. In line with this, the team should look to streamlining its current tool-kit, which contains 42 tools, by identifying lightly used tools and either discontinuing these or merging them with other tools. The team is also encouraged to conduct a user survey on its now-substantial user base to help make this determination. (The survey results are also likely to be of interest for the wider formal-methods research community.)

Additional recommendations for VASY taken from pages 4 and 8 of the evaluation report:

The main kernel of ComC is focused on well established theories of embedded systems design. They have been quite successful, but in the future a significant portion of the effort needs to be practical and to involve research tool building efforts coupled with experimentation.

The VASY project presents unique challenges in the future due to the maturity of its tool-base. Ensuring continued availability and development of the tools beyond the VASY project should be a priority of the INRIA management. Maybe it is time (especially since VASY is nearing completion) to create a separate activity specifically devoted to software development and distribution, possibly taking advantage of open source components.