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

*Vlad Rusu*

*1999-03-28*