The action VASY-RA started in January 1997. The problem area it addresses is the use of formal methods for the verification of asynchronous concurrent systems. The key technique it exploits is the enumerative exploration of state-transition system models, which are then checked against logical specifications (model-checking). The research activity of VASY-RA deals with several problems that are crucial for the applicability of model-based verification.
The first is a definition of a suitable system (as opposed to a property) specification language and its compilation towards a state-transition format that is an adequate base for verification. The action has chosen to work in the context of LOTOS language, which has the advantage of both being standardized and having a formal semantics. Contributions have been made to definition of the new version of LOTOS, E-LOTOS, and to the compilation of LOTOS and E-LOTOS.
The second area problem that is being addressed is the definition of property specification languages and of the corresponding verification methods. Here a new language, XTL, has been proposed. This language is an extension of the mu-calculus that allows the expression of properties of the data manipulated by the programs. This yields an interesting extension of the class of properties that can be specified and verified.
The third stream of activity of VASY-RA is centered around the development, maintenance, dissemination, and exploitation of a set of tools for asynchronous system analysis. This set of tools has allowed many case studies to be undertaken in various application areas.
The work done in VASY-RA is of high quality. In the LOTOS area, good contributions to language design have been made and the action has developed a high-level expertise in the compilation of LOTOS. The work on XTL is innovative, goes in a practically important direction and has yielded usable results. The tool development effort is at the cutting edge of the state-of-the-art and the case studies that have been completed are quite significant.
The publication record of the action is good, especially given all the effort it devotes to tool development and case studies. The project organizes the distribution of its tools, which effectively contributes to its visibility. It also has a strong presence at the European level.
Technology transfer is certainly a strong point of VASY-RA. Indeed, the development and distribution of tools makes research results available in a directly usable form. This is a very effective road to technology transfer. Furthermore, the various case studies that have been undertaken show the potential of technology that is being developed. Finally, the action collaborates closely with a number of industries, which both keep in touch with industrials needs and contributes to the industrial acceptance of its line of work.
The action has started a line of work that has an excellent potential for industrial impact, includes very interesting scientific contributions, and shows the high skills of its team. This line of work is definitely worth pursuing. One point for thought is the use of LOTOS. The advantages of the language are clear and the fact E-LOTOS is moving in the direction of simplification is a positive factor. However, the use of LOTOS is still quite limited and it would be unfortunate that the work of VASY-RA have a reduce impact because of the choice of LOTOS. This does not mean that switching to another language is advisable, but that, as is already done to a large extent, language independence should be sought whenever possible in the work that is undertaken. In this spirit, the work done in the action deserves to be made known as widely as possible, a goal that should be constantly pursued both on the publication and the tool distribution front. Finally, the case study work is clearly valuable, but it would be useful to organize this activity according to the specific capabilities of the tools that one wishes to test and demonstrate.
VASY-RA is a strong action that combines good scientific work, with a major tool development and case study effort. It is designed in a technology-transfer oriented way that gives it a lot of potential in this area. What it has achieved since its still recent start is quite impressive.
Back to the VASY Home Page