Deductive Proof of Software Properties
by Patrizia Asirelli and Franco Mazzanti
The aim of an recently begun IEI project is to experiment with
the idea that a deductive approach can successfully be adopted
to support the verification of properties of programs written
in high level languages.
The use of high level languages (or better, the use of safe subsets
of them) is being increasingly recommended by regulating organisations
and standards for the development of critical software. However,
when we try to nail down a precise definition of which properties
should be automatically verified during the development process,
we find a wide set of alternative definitions of safe subsets,
different degrees of supported automatic verifications, and few
available tools that might help the programmer (or verifier) in
his/her task.
Because of the intrinsic fluidity of the problem (the same project
might be constituted by different fragments with different criticality
levels and for which different sets of properties should be guaranteed),
we cannot claim that this kind of verification should be performed
by the compiler, even if it actually needs almost all the information
usually available to the compiler. The alternative, with which
we are now experimenting, is to use a deductive environment, able
to make use of all the information the compiler can gather on
the program under analysis, for expressing and verifying the set
of properties in which we are interested.
The high level language being considered in this project is Ada.
This choice has been made for several reasons. Ada subsets are
widely used for the development of critical systems (especially
in the avionic/space field). Ada is very suitable for developing
further advanced static verifications because of the richness
and intrinsic safety of its type system. Ada comes with a very
important draft ISO standard (ASIS) which defines a standard interface
allowing a compiler to export all its knowledge on a program towards
other development tools. Finally, good quality free development
environments for Ada exist and are widely used.
The deductive environment used by the project is based on Gedblog,
a deductive database management system developed at IEI and actively
maintained. The Ada compiler used in the project is the GNU based
GNAT compiler, and the ASIS library is a prototype version developed
at EPFL (Ecole polytechnique fédérale de Lausanne).
The approach with which we intend to experiment in the project
is the following. First, given an Ada program we plan to automatically
build a logical database containing all the basic properties of
the program itself, as provided by the Ada compiler through its
ASIS interface (the program syntactic structure, the static semantic
relations between its components, and whatever else might be interesting
to extract). This basic database is enriched with rules expressing
more complex properties, usable by the verifier to flexibly compose
logical queries about the program under analysis.
The project activity has just begun and is currently in a preliminary
study and experimentation phase. If the results are encouraging,
we plan to continue the activity with the verification of more
complex properties, like the absence of particular classes of
run-time errors, or the full adherence to some particular ‘safe
coding guidelines’ (whose satisfaction is too often still verified
in a non mechanical way). We are open and looking forward to possible
collaborations with other ERCIM partners interested in similar
aspects.
Please contact:
Franco Mazzanti - IEI-CNR
Tel: +39 50 593 447
E-mail: {asirelli,mazzanti}@iei.pi.cnr.it
