FLoC '02 - RT-TOOLS program

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