Achieved Results:
Lucifer: A tool for verifying Lustre programs
A tool that translates a Lustre program into a model in
propositional
logic has been developed.
The model can be used for performing induction proofs
in NP-Tools (which implements Stålmarck's method), where the
length of the
induction base (the number of times the transition function is
unrolled) is given as a parameter to the translation.
The verification method used is based on synchronous observers and
so should be compatible with other verification efforts in SYRF.
Countermodels are provided when a program fails to satisfy the
required property. Because the translation is into a hierarchical
network of components, matching the structure of
the Lustre source, these countermodels can easily be used
to trace bugs. The graphical interface of NP-Tools is useful here.
Earlier Lustre to NP-Tools translators produced a large flat formula,
making fault-finding difficult.
In an exciting recent development, Ed Clarke and his group have introduced the notion of bounded model checking - in which state-space exploration is limited to a certain number of steps. The method was presented in an extra talk at the recent conference on Formal Methods for CAD. This form of model checking can be coded in propositional logic so that it reduces to boolean satisfiability. First experiments in Clarke's group indicate that Stålmarck's method works very well in this context. We have begun to incorporate bounded model checking into the Lucifer tool.
Lucifer has been used to analyse a number of case studies (for example Volvo's cruise controller example, CRISYS example of a train system). Work on Schneider's case study has just begun. The Lucifer tool is documented in Magnus Ljung's Master's thesis, which is currently in draft form. Work on Lucifer has been partially funded by SYRF.
Reducing proof hardness in Stålmarck's method
Work has continued on the addition of extra definitions of fresh
variables to system formulas in order to reduce proof hardness.
The extra definitions, which we call helper variables
increase the set of subformulas available to the
prover and can reduce branching and so proof complexity.
The approach is outlined in the workshop paper by Sheeran and Borälv
listed below.
This year, we have concentrated on using helper variables in doing
purely propositional proofs.
Last year, we verified arithmetic circuits across levels of
abstraction
and so made heavy use of the integer arithmetic with which
Stålmarck's method has been extended.
We have studied the well-known pigeon hole formulas, which in their
standard form have proof hardness degree that increases with size.
We have reformulated them recursively, adding many new variable
definitions of recursive sub-formulas, to reduce the hardness degree
to
one independent of size.
Now, we are working on applying the lessons learned in this abstract
setting
to verification of synchronous circuits and programs.
We have had some success in reducing the hardness of bit-level
multiplier
verification but we have so far been unable to reduce the hardness
degree
to a constant independent of size. This remains our goal.
As part of this work, we have worked on reducing the hardness of
proofs of some adder circuits received from SYRF partners.
The Lava system that we use to generate formulas from Lustre-like
programs has been described in a paper presented to the International
Conference on Functional Programming.
A tutorial on Stålmarck's method
A tutorial paper on Stålmarck's method has been written.
An expanded version will be submitted for journal publication. The
tutorial
appears as an annex to Deliverable 0.2.2.
Publications: