Achieved Results:
Lucifer, A tool for verifying Lustre programs: refinement and
applications
The Lucifer tool for verifying Lustre programs has been further
refined
during the third year of the project.
The tool translates a Lustre program into a model in
propositional
logic, by extracting the transition function.
The model can be used to perform
inductive proofs
of safety properties ; the
length of the
induction base (the number of times the transition function is
unrolled) is given as a parameter.
The verification method used is based on synchronous observers and
so is compatible with other verification efforts in SYRF.
Counter-models 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 counter-models can be used
to trace bugs.
This year, we have implemented a number of number of additional constraints on the sequences of states considered in the inductive proofs. The use of additional invariants strengthens the proof method. The first of these, the constraint that all states in the considered path must be different, allows us to make a complete model checker for safety properties, and so is clearly justified, even though it can give rise to large formulas. In the examples tried so far, these formulas have proved to remain easy as we turn up the length of the induction base. However, further experiments are necessary to confirm that this is the case on a variety of sizes and types of state transition systems. Unfortunately, more complicated constraints, such as attempts to restrict to locally shortest paths have not so far paid off. This is a disappointing result. The next step is to explore the use of Quantified Boolean Formulas (QBF) formulas, and their translation to propositional logic, in the constraints. The necessary formulas have been defined. A draft paper describes this method of verification using induction with constraints, and ends with a presentation of the necessary QBF formulas to ensure that the method does not iterate beyond the diameter of the state machine.
Viewing traces of Lustre programs
In an initial feasibility study, Lucifer has been extended to generate
formulas for transition functions
in Many Sorted First Order Logic (MSFOL) with bounded domains, instead
of in NP-Tools macros.
Using the technology developed during
the FAST project (Esprit project
number
25581), the resulting
formula is translated to propositional logic, and a "test objective"
(a constraint in MSFOL) can be added.
The models then generated (using Prover) can be viewed in the FAST
Graphical User Interface.
Applications of Lucifer
Lucifer has been used to analyse a number of case studies, some
of them industrial projects or pilot studies.
Current industrial projects are leading to demands for increased
functionality in Lucifer, and the tool is under active development.
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 sub-formulas available to the
prover and can reduce branching and so proof complexity.
However, this has not been a high-priority activity.
The work has been superseded by the development of new proof
strategies
for propositional logic theorem proving.
Journal version of the tutorial on Stålmarck's method
The tutorial about Stålmarck's method that was written during
year 2 of the project was selected to appear in a special issue of
the journal Formal Methods in System Design, to appear in January 2000.
It is very much revised and extended, and is an important
documentation of the method, which had not previously been
sufficiently exposed in the literature.
The
tutorial
appears as an annex to Deliverable 0.2.3.
Publications: