Evaluation Report on INRIA INRIA Research Theme ComC (excerpt)
The evaluation of VASY was performed by the following panel members:
- Rance Cleaveland, University of Maryland & Reactive Systems Inc.
- Luciano Lavagno, Politecnico di Torino and Cadence Berkeley Labs
- Ugo Montanari, University of Pisa
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.
- Applications of static analysis techniques to improved state-space generation;
- New approaches for "on-the-fly", memory-efficient verification;
- New case studies in hardware-design and biological system analysis; and
- Engineering improvements in the core compilers, and the implementation of translators from other modeling languages to the core CADP notation, LOTOS.
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
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
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
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
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
The evaluation team has two recommendations for the coming term of the
- 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.
- 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.