1996-1997: Continued work after PhD.

As an assistant at the University of Nantes ( Nantes Technical Institute (IUT), department of Computer Science & Electrical Engineering) I have continued working for one year on these topics. The previous results (decidability of time-bounded TCTL) were extended to the full logic, but for a more restricted class of automata (the strongly non-Zeno and uniformly-periodic hybrid automata). This class still allows to model some interesting real-time applications: systems composed of tasks which are not preempted too often such that each task manages to terminate within bounded time [RR96] and systems whose tasks are periodic  [R97] . Furthermore, in partnership with Augusto Burgueno and Frederic Boniol (researchers from French National Institute for Avionics Research in Toulouse), we have developed a kind of "parametric verification": synthesizing conditions on the task speeds of a real-time system, for a given safety property to hold. We have introduced a model called Slope-Parametric Hybrid Automata (SPHA) and designed a semi-algorithm for the analysis of this model, which terminates for a subclass of SPHA similar to the strongly non-Zeno [BBR+97,BR97] . A prototype tool in Maple and Prolog was implemented, that we have applied to a simple task-control example [BR97] .