RT-TOOLS program

Thursday August 1st, 2002


All sessions take place in auditorium 10.

RT-TOOLS's program is also available with abstracts or side by side with other meetings.

09:15-10:30  Session 1: Design and Synthesis

09:15  Welcome
09:30  Goran Frehse, U Dortmund, Germany
Solving simulation relations of timed automata for the design and verification of timed discrete controllers
10:00  Robert P. Goldman, Smart Information Flow Technologies, USA; Michael J. S. Pelican, Honeywell, USA; and David J. Musliner, Honeywell, USA
Verifier trace-directed backjumping for controller synthesis

10:30-11:00  Refreshments

11:00-12:30  Session 2: Model-Checking

11:00  Jesper Møller, IT U of Copenhagen, Denmark
Simplifying fixpoint computations in verification of real-time systems
11:30  Gilles Audemard, Alessandro Cimatti, Artur Kornilowicz, and Roberto Sebastiani; ITC-irst, Italy
Bounded model checking for timed systems
12:00  Dragan Bosnacki, Eindhoven U of Techn., The Netherlands
Partial order and symmetry reductions for discrete time

12:30-14:00  Lunch

14:00-15:30  Session 3: Tool Development

14:00  Karine Altisen, INRIA Rhône-Alpes, France and Stavros Tripakis, IMAG Grenoble, France
Tools for controller synthesis of timed systems
14:30  Alexandre David, Uppsala U, Sweden; Gerd Behrmann, Aalborg U, Denmark; Kim Guldstrand Larsen, Aalborg U, Denmark; and Wang Yi, Uppsala U, Sweden
New uppaal architecture
15:00  Anton Cervin, Dan Henriksson, Bo Lincoln, and Karl-Erik Årzén; Lund Inst. of Techn., Sweden
Jitterbug and TrueTime: Analysis tools for real-time control systems

15:30-16:00  Refreshments

16:00-17:00  Session 4: Applications

16:00  Béatrice Bérard, ENS Cachan, France; Patricia Bouyer, Aalborg U, Denmark; and Antoine Petit, ENS Cachan, France
Analysing the PGM protocol with uppaal
16:30  Martin Carlsson, Enea OSE Systems AB, Sweden; Jakob Engblom, IAR Systems AB, Sweden; Andreas Ermedahl, Uppsala U, Sweden; Jan Lindblad, Enea OSE Systems AB, Sweden; and Björn Lisper, Mälardalen U, Sweden
Worst-case execution time analysis of disable interrupt regions in a commercial real-time operating system