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
