Evaluation Report on INRIA Programme 1C (excerpt)
The evaluation was performed by the following panel members:
- Michel Bidoit, LSV, CNRS&ENS de Cachan (France)
- Luca Cardelli, Microsoft Research, Cambridge (UK)
- Rance Cleaveland, Stony Brook University & Reactive Systems Inc. (USA)
- Nicholas Halbwachs, Verimag Grenoble (France)
- Stuart Kent, University of Kent & IBM Consultant (UK)
- Mogens Nielsen, University of Aarhus, (Denmark)
- Daniel Pilaud, PolySpace Technologies (France)
- Dominique Potier, Thales Research & Technologies (France)
- Bernhard Steffen, University of Dortmund (Germany)
The Vasy project focuses on techniques for designing and verifying properties of
asynchronous communicating systems of processes. In contrast with synchronous
systems, the individual processes of asynchronous ones may execute at widely
differing rates, although they can also synchronize on occasion to exchange data. The
importance of asynchronous systems cannot be overestimated: applications as diverse
as wide area networks and multiprocessor computer architectures rely integrally on
The thesis underpinning the scientific research of the Vasy team is that improving
how asynchronous systems are designed in the future will require the use of
mathematics, or "formal methods". This thesis has given rise to three main areas of
research to date:
In its work, the Vasy team confronts several scientific and engineering challenges.
Among the former are the design of modelling languages and algorithms for checking
properties of large asynchronous systems. The latter include the design of efficient
tool boxes with wide applicability and practical utility. In general, the project is
engineering-driven, with the tool-building agenda driving the theoretical one.
- Modelling languages: The team has participated in the development of
formalized notations for describing asynchronous systems and of tools for
generating low-level, easy-to-analyze models from higher-level, user-friendly
- Verification tools: The team has developed an array of tools for assessing the
behaviour of system models
- Industrial case studies: The team has collaborated with several industrial
partners to apply the project's results to industrial design problems.
The Vasy project is engaged in highly significant and important work. The utility of
mathematical modelling in the traditional synchronous sphere of hardware is
unquestioned; asynchronous (traditionally, software) systems lack a similar basis for
rigorous design and mechanical analysis. Traditional design practice too often relies
on ad hoc, organization-specific, labour-intensive development strategies, owing in
part to the lack of generally accepted mathematics and associated analysis routines. It
is this lack that drives the research of the Vasy project and defines its importance.
Vasy has existed as a project since 2000, although in the three years leading up to its
inception as a project it functioned as a research action. In 1999, this research action
underwent its last evaluation. The current report will focus on team achievements
since 2000, although parenthetical comments on work since 1999 (the most recent
evaluation) will be made from time to time.
Scientifically, the Vasy project conducts research of very high quality. This is
documented in several aspects: the number and quality of the scientific publications
of the team; the wide dissemination of software written by the team; the participation
of team members in organizing high-profile international symposia and workshops;
and the achievements of recent PhD graduates from the team.
As noted in the summary, the Vasy project has a significant engineering component,
and many of the team members have a primary responsibility for engineering
activities relating to the development and deployment of the Caesar/Aldebaran
Development Package (CADP), the main software package released by the project.
Thus, while the team consisted of 14 persons at the time of this evaluation, not all 14
would be expected to produce scientific publications. This fact makes the scientificpublication
output (14 since 2000, 21 since 1999) reasonable, and even more than
might be expected, given the relatively low levels of publishing exhibited by
traditional systems researchers.
Of course, the relatively high numbers of engineers participating in the team would
raise the expectations for systems-related output, and the team has performed
outstandingly in this regard. The CADP system has been in distribution since the mid-
90s; the last major release of the system was at the end of 2001, although several
patches have been released since then. The software has been licensed to 283 different
sites around the world, and over 2,500 different machines. This makes it among the
most popular non-USA-originating verification tools. More about the growing use of
CADP may be found in the technology transfer section below.
The scientific achievements of team members are reflected in their participation in
program committees of international conferences and workshops. H. Garavel was a
program committee member on nine different committees since 2000 (13 since 1999)
and chaired the committees for the International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, the premiere European tools
conference, in 2003, and the ERCIM International Workshop on Formal Methods for
Industrially Critical Systems in 2002. R. Mateescu has taken part in four such
program committees during this time.
Finally, R. Mateescu, who received his PhD as part of the Vasy project and now is a
CR, received the IT Award from the Fondation Rhône-Alpes in 2002 for his modelchecking
tool developed as part of the CADP system. M. Sighireanu, who received
her PhD as part of the Vasy research action in 1999, is now an assistant professor at
Regarding the specific research activities undertaken by the team, as noted above,
these fall into three categories: modelling languages, verification tools, and industrial
case studies. The remainder of this section assesses each of these in turn.
Modelling languages: The main contributions of the team in this area fall into three
categories: the design of E-LOTOS, an ISO standard notation for modelling
asynchronous systems; the design of a new intermediate format, New Technology
Intermediate Format (NTIF), into which E-LOTOS and other asynchronous languages
may be compiled; and compilation techniques for E-LOTOS. The research in this area
is competent, especially the design of NTIF. In many verification projects too little
attention is paid to issues like compilation, intermediate formats, etc.!; all focus is on
the analysis routines, to the detriment of the performance actually experienced by a
user. The E-LOTOS language appears to be a thoughtful extension of LOTOS,
although there is a danger that the team focuses too much on E-LOTOS (because it is
a standard) rather than other languages (e.g. SystemC) which, although not standards,
are much more widely used than E-LOTOS. However, in defence of the Vasy team it
should be noted that formal notations with support for message passing and data are
still not in widespread use: the team's promotion of E-LOTOS is thus occurring in
something of a vacuum. On the other hand, the E-LOTOS-related publications are
few, and the downloads of the E-LOTOS-related software much smaller than for the
team's other tools.
Verification tools: The project's contributions in the area of verification tools are
superb. The CADP system is organized as a large collection of small sub-tools
oriented around a common set of APIs. These APIs include ones for basic system
models (automata), encoding schemes (binary decision diagrams, binary-coded
graphs), etc. Numerous additional sub-tools have been added to CADP since 1999,
including various routines for checking logical properties of system models;
minimizing system models; a framework for on-the-fly checking of system properties;
compositional abstraction tools; tools for distributed model checking; tools for
computing performance measures of probabilistic system models; and a scripting
language for verification. This design strategy - lots of "lots of little tools" - is a
significant departure from the traditional "one big tool" system architecture of
traditional verification tools, and a much needed one: by exposing what are
traditionally internal interfaces, CADP is much easier to interface with other tools.
The research undertaken by team members into model-checking algorithms for
different fragments of the modal mu-calculus is driven directly by tool considerations,
and the resulting routines led to R. Mateescu's receipt of the IT Award from the
Fondation Rhône-Alpes in 2002.
Case studies: The project's case-study component is very compelling. Extensive
collaborations with Bull, and contracts with Alcatel, Schlumberger, MGEUPS/
Scalagent/Silicomp, and Engineering/Thésame, graphically demonstrate the
team's commitment to assessing the results of its research in practice. The outcomes
of the Bull project are particularly impressive, with several subtle yet important issues
with Bull's testing methodology for its cache-coherency protocols.
Given Vasy's engineering orientation, one would expect a significant technologytransfer
component to its work, and this is indeed the case. The team currently derives
90% of its project funding from industrial contracts. Its partners include a number of
large and small French and European companies; readers are referred to the
"Industrial Case Study" part of the previous section for more details. Members of
Bull's technical staff have worked, and continue to work, as members of the Vasy
team. It should be noted that the analytical power of CADP appears to represent the
"draw" for these contracts; the team's dependence on E-LOTOS may discourage
some industrial collaborations.
Vasy scores extremely well in this category. Parts of the CADP software have been
used by other INRIA projects, including Triskell and Vertecs in the 1C Theme and
Lemme, Oasis, Lande, Apache and Sarde in other themes. The group is also active in
collaborating with non-INRIA research groups (Isima/Limos, Liafa, LSR-IMAG, and
Verimag) and international groups. This last features impressive collaborations on
tool development with the University of Twente in the Netherlands and a host of
protocol verification activities with universities in the UK, Canada, Hungary, and
The project is led by H. Garavel, who exercises strong scientific and administrative
leadership. Within the team, responsibilities seem to be agreed upon rather than
allocated in a top-down manner. The team also has an annual multi-day retreat to
review the previous year's activities and plan the current year's. This is an excellent
idea that we think other teams could also profit from.
The team has identified five areas that it expects to pursue in the coming four years:
These topics represent logical extensions of the team's current efforts, and they are
likely to make progress on all of them.
- Implementation of E-LOTOS: The proposed effort would on the one hand add
support for features of E-LOTOS not currently supported in the current tool set
(exceptions, modules, etc.). On the other, it would merge currently distinct code
- Model checking with data: The proposed effort would extend existing CADP model
checking support for processes without data (diagnostic procedures, on-the-fly
analysis) to systems that manipulate data.
- State explosion: To combat combinatorial problems inherent in verification, the team
proposes to study compositional verification techniques as well as static-analysis
techniques on the NTIF format and distributed model checking.
- Generic components for simulation, verification and testing: The idea here is to
adapt the CADP APIs to support the development of language-independent
"simulation and testing" engineers. Particular research issues involve representation
and manipulation of data.
Conclusions and recommendations
Vasy has an excellent verification toolset, CADP, substantive and deep collaborations
with industry and other research groups, and an adequate modelling-language
compilation toolset built around the E-LOTOS language. The scientific output of the
team is of high quality and likely to remain so.
The team does face several risks as it pursues its future plans, and we list these below.
The team has reasonable strategies for all but the first: keep building generic tools,
develop the user community as a means both of locating new case studies and
recruiting new students and team members, institutional improvements to improve
relations with local universities. There does seem to be a "blind spot" in team
leadership with respect to E-LOTOS, however: the response to questions about ELOTOS
has been that E-LOTOS is better than other design notations and thus is
bound to succeed. We believe a more nuanced argument would serve the team better.
On the one hand, the number of mathematically precise modelling notations with
value-passing and asynchronous concurrency is indeed small, and E-LOTOS is as
reasonable as any existing language to build a tool set for. However, E-LOTOS lacks
many features in modern (informal) design notations: objects, topology
reconfiguration, etc. And other notations, while lacking some of the compelling
features of E-LOTOS, have a much larger user base: SystemC, STATEMATE, etc. A
more compelling argument for E-LOTOS would therefore be that advanced compiling
techniques developed for E-LOTOS are likely to be necessary for other notations that
include asynchronous concurrency. And then papers justifying this assertion should
- Over-emphasis on E-LOTOS. The team's presentation lists E-LOTOS as its
first, and presumably most internally important, research direction. However,
the research direction with arguably the greatest impact is the CADP research.
There is a danger that the former will drain resources from the latter. There is
also concern that the team places too much faith in the standardization of ELOTOS
as evidence of the eventual commercial impact of the language.
- Lack of industrial interest in formal methods in favour of semi-formal
methods. This is an often cited concern about all formal-methods research. On
the other hand, given the alternatives, this concern is, we believe, misplaced;
the real risk is not a belief in the importance of mathematics by practitioners,
but rather the lack of standardly available mathematical notations for system
modelling and training of engineers.
- Team instability will have a negative impact on tool development. This is an
important point, and the team expressed concern about INRIA's inability to
grant long-term contracts to software engineers.
- A lack of students will impede the ability of the team to develop the next
generation of Vasy members. The team cited difficulties in obtaining
permission to teach upper-level courses at local universities as a particular
frustration in their current setting.
- The overdependence on Bull for industrial funding could lead to project
dislocation if Bull is unable to continue and no similarly sized industrial
partner is found.
Regarding other recommendations, the project would of course benefit from
establishing a relationship with another major industrial partner like Bull. Mention is
made of embedded systems as a targeted application domain over the next four years;
making connections with a major automotive, aerospace, or other heavy-engineering
enterprise may provide a useful direction for new partners. A willingness to consider
design notations other than E-LOTOS may be beneficial in this respect.
Back to the VASY Home Page