1992-93: MSc Thesis.
My initial work is based on the reactive language ELECTRE
developed by my supervisor Prof. Olivier Roux at
Ecole Centrale de Nantes .
I started working on this topic by studying the connections between ELECTRE
and the GRAFCET, a french standard language for process
automation. This has lead to a publication in a french journal [RR94]. Then,
I was guided towards the verification of timed properties of ELECTRE
programs, such as ``the control task terminates in at most 3 milliseconds''.
This lead us to investigating models such as timed and hybrid automata
and real-time temporal logic.