Approach:

This task aims at providing methods and tools for applying deductive tools to synchronous programs that cannot be model-checked. As examples, the chosen synchronous language was Lustre and the deductive proof tool was PVS . In the course of the project, the Irisa team working on Signal joined the task and proposed another instanciation, based on Signal and the proof assistant tool Coq

There was also some work on deductive proofs performed by the team at Linköping, using NP-Tools by Prover. This work was integrated in the study
on hybrid systems under work package 7. However, some reference to the work is made here for the sake of completeness.

Achieved Results:

• Several significant applications have been identified and experimented:
• An emergency braking system.
• The SteamBoiler example .
• A climatic chamber case study (see Annex.3.4.c)
• Two approaches have been prototyped:
• A Signal-Coq one based on co-induction and mu-calculus (see Annex 3.4.3.a).
• A Lustre-PVS one, based on Kahn semantic and also mu-calculus (see Annex 3.4.3.b).

At the end of the project, we come up with two approaches: the Lustre-PVS one and the Signal-Coq one, which seem to operate quite satisfactorily. Unfortunately, we have not been able to make comparisons between them and this remains to be done, both theoretically and from the efficiency point of view.

Also, the question of scalability has to be better investigated. One possibility could be to study some refinement-based design method, adapted to the synchronous programming context. Another possibility could consist of investigating the cooperation between model checkers and theorem provers.

Application in the hybrid system area needs to combine the proofs on the controller with some continuous analysis, in our case using MatrixX simulation models.

Annexes:

• D. Nowak, J-R. Beauvais, J-P. Talpin. Co-inductive axiomatization of a synchronous language . In proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics. LNCS 1479 , October 1998.
• C. Dumas. A PVS proof obligation generator for LUSTRE . Research report, 1999.
• S. Nadjm-Tehrani, O. Åkerlund. Combining theorem proving and continuous models in synchronous design; In proceedings of the World Congress on Formal Methods, Toulouse, France, September 1999, Volume II, LNCS 1709, pages 1384-1399, (C) Springer Verlag.