SYRF Project



Task 3.3: "Handling properties depending on numerical variables"

Abstract of deliverable 3.3.1

Back to the SYRF Home Page



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:

Achieved Results:

Publications:

  1. 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