SYRF Project
Task 3.2: "Use of the Stålmarck Method"
Abstract of deliverable 3.2.3

Back to the SYRF Home Page
Back to Deliverables

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:

  1. Mary Sheeran and Gunnar Stålmarck.
    A tutorial on Stålmarck's proof procedure for propositional logic. To appear in Formal Methods in System Design, 16:1, January 1999.

  2. Mary Sheeran and Gunnar Stålmarck.
    Checking safety properties of finite state systems using induction and boolean satisfiability. Draft paper, 1999.

  3. Gunnar Stålmarck.
    Stålmarck's method with extensions to Quantified Boolean Formulas (short abstract of invited talk). In Proceedings of the Eleventh International Conference on Computer Aided Verification, LNCS, Springer Verlag, 1999.