Evaluation Report on INRIA Programme 1C (excerpt)

June 2003

The evaluation was performed by the following panel members:

Vasy

Summary

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 asynchrony.

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.

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.

Scientific evaluation

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 Paris VII.

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.

Technological transfer

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.

Cooperation

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 Sweden.

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.

Future plans

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.

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 be written.

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.


VASY logo Back to the VASY Home Page