1993-1996: PhD Thesis.

My work (under the supervision of Prof. Olivier Roux ) consisted in using and adapting existing formalisms for the verification of ELECTRE programs. I started by searching for results in the literature, among which the following is most relevant for our topic: model checking of the temporal logic TCTL is decidable on timed automata, but it is undecidable for hybrid automata. The logic TCTL is suitable for expressing most properties of interest for ELECTRE programs. But for modeling the programs themselves, we need a subclass of hybrid automata that strictly includes timed automata. This is because timed automata may only have continuously running clocks, while the ``task-preemption'' operation in ELECTRE does require ``freezing'' of clocks. Therefore, my work consisted in finding a subclass of hybrid automata expressive enough for modeling ELECTRE programs, while still decidable for a fragment of TCTL powerful enough to express time-critical properties. This lead to defining the so-called strongly non-Zeno hybrid automata, characterized by the following: all cyclic runs have a minimal duration uniformly low-bounded by some strictly positive real, and all finite runs can be continued at infinity. I have then obtained:

• theoretical results: translation of ELECTRE programs into strongly non-Zeno hybrid automata, following systematic rules that guarantee correctness; and decidability of the time-bounded fragment of logic TCTL on strongly non-Zeno hybrid automata. Furthermore, the strongly non-Zeno quality is decidable for an arbitrary linear hybrid automaton. These results [R96,RR96,RRC] allow to express and to verify, in principle, the most critical properties of ELECTRE programs, as well as other reactive applications based on similar hypotheses.

• an implementation of prototype tool VALET, to verify time-critical properties of ELECTRE programs. Time-bounded safety and time-bounded response can be verified with this tool, after a given ELECTRE program has been translated (automatically and following the systematic rules in the theory) into a hybrid automaton. The tool uses a polyhedral-calculus package for hybrid systems model-checking.

• towards the industrial application of the tool, I co-supervised a Master's Thesis on using VALET in an experiment at SNECMA (main french airplane motor constructor) for verifying time-critical properties of the control task of an airplane motor under development. Although partial, the results were encouraging, which lead the industrial partner to fund a PhD grant for our student, Patrice Boisieau, to develop an industrially relevant verification tool.