Symbolic Techniques for Program Analysis
by Henk Nieland
As a consequence of our ever increasing dependence on the proper
functioning of software systems, the need for proving their reliability
has to be taken serious indeed. Until recently such proofs were
only feasible for systems whose size is far below what is found
in practice. Recently developed techniques, however, may offer
a solution. The aim is now to apply these techniques effectively,
so that real-life systems can be successfully analyzed. By combining
mathematical rigour with manual computation CWI developed methods
which can prove ‘beyond reasonable doubt’ the reliability of software
systems of a realistic size.
In principle there are three approaches: proof by manual labour,
fully automated proof techniques, and a mix between the two. CWI
has shown that the last way enables the analysis of realistic
systems.
Manual proof can be carried out in the context of Process Algebra
(PA). The use of PA has advantages above other verification methods
such as modal or temporal logic because of its high level of abstraction
and its composition properties. A basic tool is the Cones & Foci
Theorem, which effectively can be used to prove statements of
the form: Specification = Implementation. On the basis of PA,
CWI developed mCRL (micro Common Representation Language). The
idea was to create a basis for sharpening symbolic techniques,
rather than adding another language to the repertoire. With mCRL
one can carry out proofs manually following strict logical rules.
In practice, however, several such proofs remain ‘sloppy’, because
the manual method is effective only for small systems, not exceeding
one page of code.
Fully automated proof techniques are usually based on state automata.
At CWI now systems with 108 states can be dealt with (in general
the limit is 106), but realistic systems are still considerably
larger. An even not really large system such as the software used
for the safety of a small railway-yard, which was recently analyzed
by CWI using propositional logic, consists of about 101000 states.
Of course, it is of the utmost importance to find ways to reduce
the number of states. Our research indicates that by transforming
processes described in mCRL to a normal form (Linear Process Operation)
using rewriting techniques (automated induction, tree automata),
exponential reduction of the number of states can be reached.
Since neither purely manual, nor purely automated techniques can
cope with realistic systems, a compromise must be sought. By using
proof checkers, which guarantees the required precision, in combination
with manual control, CWI has reached promising results. Experience
with checkers like Coq, PVS, and Isabelle, used in this way, shows
that this approach can be effective for middle-sized systems.
One may compare this hybrid technique with the way packages such
as MATLAB and MAPLE are used in mathematical formula manipulation.
This approach to putting formal proof techniques to practical
use may in due course very well lead to a revolution in mathematical
argumentation, as was foreseen already some thirty years ago by
the eminent Dutch mathematician N.G. de Bruijn when he created
his Automath system.
Meanwhile several instances of faulty software have been revealed
by applying formal proof checkers under manual control. Recent
Dutch examples include the automated control system for the legs
of car lifting installations in garages, and for the doors of
the dam in the Nieuwe Waterweg which protects the Rotterdam area
by closing the doors in case of flood. Sincs many more such instances
can be expected to show up in the near future, we may see before
long the birth of a new profession: that of software prover.
More information can be found at http://www.cwi.nl/~jfg/
Please contact:
Jan Friso Groote - CWI
Tel: +31 20 592 4232
E-mail: JanFriso.Groote@cwi.nl
