ERCIM News No.36 - January 1999

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