ERCIM News No.37 - April 1999

Software: Objective Zero Defect

by Maurice Mashaal

---

To write programs that are at the same time complex and without logical faults or bugs, that is a feat, or more likely a utopian dream. In a day and age when computers are everywhere, one cannot help but be a little anxious at moments: isn’t there any risk that the people who deal with my credit card will fleece me without my noticing it? Are all the electronic circuits of the plane I am about to board entirely compatible with one another? In general, the software at work has been validated and tested beforehand, all the more so if its malfunctioning can have grave consequences. Validation and testing take time and effort, however, which cost money. Furthermore, how can we be sure that everything was verified?

This is the interest of research that aims at systematizing and automating such procedures. The problem arises foremost for distributed or parallel systems that comprise several communicating or interacting elements. For example, communication protocols must be certified to be locking free to avoid situations in which two different programs are waiting for each other to supply an information that is necessary for them to keep executing or in which several programs need to write simultaneously at the same memory address.

Such research is being carried out by several INRIA projects, with a significant theoretical aspect. In effect, one of the approaches consists in analyzing the semantics of the programming language to obtain formal models of the software under consideration. This step facilitates the design of the actual software verification tools. The verification can in fact be effected by trying to formally prove properties and good functioning criteria. However, most often verification entails a recourse to brute force, that is to say to observe the behavior of the system for each set of data. This procedure is equivalent to exploring all the states that the system comes to occupy, which are modeled by a ‘states graph’.

The problem is that the number of configurations to be explored is immense, even if the elements of the system can only occupy a finite number of states, which is often the case in practice. The difficulty thus resides in carrying out this exploration in an ‘intelligent’ way, by restricting attention to significant cases or to sub-systems and so on. This can avoid a comprehensive verification that would be way too costly in terms of time and memory. In addition, the goal is to design tools that can be used by non-specialists. This is far from being a negligible aspect if one has industrial applications in mind.

MEIJE

One of the projects that are working in this direction is MEIJE, which is interested in particular in the Esterel language. Esterel is a programming language developed within MEIJE that is adapted to command systems that must react in real time to an external environment and function in a ‘synchronous’ fashion between parallel components. The applications considered by MEIJE thus naturally concern embedded systems for aircraft, automobiles, or material circuits among others. This is an area where software reliability is crucial. MEIJE is thus working in collaboration with Dassault Aviation on the modeling of embedded systems in aircraft for their verification. Similarly in micro-electronics, MEIJE is experimenting on the use of Esterel techniques for the synthesis and design of integrated circuits. From a formal viewpoint, such devices are equivalent to concurrent software systems.

The VASY Initiative

The VASY initiative is contributing to the development of a compilation and verification toolbox called CADP and already distributed to more than 172 sites worldwide. This environment is constructed around LOTOS, a language that makes it possible to describe protocols for ‘asynchronous’ distributed and parallel systems. LOTOS was chosen because it is the only language of this type that has the status of an international standard and whose semantics are rigorously defined.

Applications of the CADP toolbox range from databases to communication networks including cryptographic security protocols for electronic commerce. CADP is being currently used by Bull, in the framework of the Bull/INRIA Dyade GIE, to validate the multiprocessor architectures that the company is devising for their future high end servers. CADP was also used to detect an error in the ‘Firewire’ bus (IEEE standard 1394), a high speed serial bus for micro-computers that was adopted by the main computer manufacturers, software publishers and audiovisual equipment manufacturers. This error was practically impossible to catch by hand since it only occurs after a very definite sequence of some fifty operations!

PAMPA

The PAMPA project is developing validation tools in the framework of the UML (Unified Modeling Language) object-oriented method, among others. This method is widely used in industry to write programs and model them. One of PAMPA’s strong points is the joint development with CNRS laboratory Vérimag of a software called TGV (Test Generation with Verification) that automatically produces compliance tests. With this tool, PAMPA for example is collaborating with the European project Modistarc whose goal is to set up a testing methodology for embedded communication and management protocols in automobiles. A large part of the applications of verification tools however concerns the field of telecommunications, in which systems are distributed in essence. Together with four other INRIA teams, PAMPA is collaborating with Alcatel in the design of tools for formal operations within a telecommunication software development line defined by Alcatel.

For more information see:
MEIJE: http://www-sop.inria.fr/meije/meije-eng.html
VASY: http://www.inrialpes.fr/vasy
PAMPA: http://www.irisa.fr/pampa

Please contact:

Robert de Simone - INRIA (MEIJE)
Tel: + 33 6 92 38 7941
E-mail: Robert.De-Simone@inria.fr

Hubert Garavel - INRIA (VASY)
Tel: + 33 4 76 61 52 24
E-mail: Hubert.Garavel@inria.fr

Claude Jard - CNRS (PAMPA)
Tel: +33 2 99 84 71 93
E-mail: Claude.Jard@inria.fr