SYRF Project
Task 3.3: "Handling properties depending
on numerical variables"
Abstract of deliverable 3.3.1
Approach:
Any synchronous program can be viewed as an interpreted automaton.
Existing verification tools for synchronous programs are based on the control
structure of the automaton, and ignore its interpretation. Task 3.3 of
the project is devoted to obtaining more precise results by means of two
approaches:
- A static method, whose goal is to cut, in the automaton, transitions
that are guarded by unfeasible conditions. Interesting results can be obtained
using a procedure checking the satisfiability of systems of linear constraints.
- A dynamic method, which takes into account the dynamic behavior
of numerical variables, by building, in each state of the automaton a system
of linear constraints invariantly satisfied in this state by the
numerical variables.
Achieved Results:
- Our approach is strongly based on symbolic computations about systems
of linear constraints, performed by the library of the tool Polka [1].
The complexity of these computations heavily depends on the number of involved
variables. To reduce this complexity, the library has been adapted to separately
handle independent sets of variables, i.e, to work on cartesian products
of polyhedral domains.
- A longer term research concerns an improvement of the dynamic method.
This method starts from an explicit version of the interpreted automaton,
which appears to be too big in practical applications. So, our goal is
to progressively refine an initially rough control structure, taking into
account the property under verification.
Publications:
- N. Halbwachs, Y.E. Proy and P. Roumanoff
Verification of real-time systems using linear relation analysis
Formal Methods in System Design, vol. 11, nr. 2,
pages 157-185. August 1997.
Annex A.3.3.1a