Wednesday September 22, 2004 |
|||||
Morning |
Afternoon |
||||
|
9:00 - 9:25 |
Registration |
14:00
- 14:30 |
A Unified Fault-Tolerance
Protocol Paul Miner, Alfons Geser, Lee Pike, and Jeffrey Maddalon |
||
| 9:25 - 9:30 |
Opening |
14:30 - 15:00 | Automating the
Addition of
Fail-Safe
Fault-Tolerance: Beyond Fusion-Closed Specifications Felix C. Gärtner and Arshad Jhumka |
||
|
9:30 - 10:30 |
|
15:00 - 15:30 | Modeling and Verification
of a Fault-Tolerant Real-time Startup Protocol using Calendar Automata Bruno Dutertre and Maria Sorea |
||
| 10:30
- 10:45 |
Coffee break | 15:30 - 15:45 | Coffee break | ||
| 10:45 - 11:15 | Formal Verification of an
avionics sensor
voter using SCADE Samar Dajani-Brown, Darren Cofer, Amar Bouali |
16:00 - 16:30 | Decomposing Verification of
Timed I/O Automata Dilsun Kaynar and Nancy Lynch |
||
| 11:15 - 11:45 | Static fault-tolerant
scheduling with ``pseudo-topological'' orderings Catalin Dima, Alain Girault, Yves Sorel |
16:30 - 17:00 | The Influence of Durational
Actions on Time
Equivalences Harald Fecher |
||
| 11:45 - 12:15 | Towards a
methodological
Approach to
Specification and Analysis of Dependable Automation Systems Simona bernardi, Susanna Donatelli, and Giovanna Dondossola |
||||
Thursday September 23, 2004 |
|||||
Morning |
Afternoon |
||||
|
9:00 - 10:00 |
|
14:00 - 14:30 | Bounded Model Checking for
Region Automata Fang Yu, Bow-Yaw Wang and Yao-Wen Huang |
||
| 10:00
- 10:15 |
Coffee
break |
14:30 - 15:00 | Some Progress in
Satisfiabilty Checking for Difference Logic S. Cotton, E. Asarin, O. Maler and P. Niebert |
||
| 10:15
- 10:45 |
On two-sided approximate
model-checking: problem formulation and solution via finite topologies J.M.Davoren, T.Moor, R.P.Gore, V.Coulthard, A.Nerode |
15:00
- 15:30 |
Model-Checking for Weighted
Timed Automata Thomas Brihaye, Véronique Bruyère, Jean-François Raskin |
||
| 10:45
- 11:15 |
On timed automata with
input-determined guards Deepak D'Souza and Nicolas Tabareau |
15:30 - 15:45 | Coffee break | ||
| 11:15
- 11:45 | Symbolic model checking for
simply-timed systems N. Markey and Ph. Schnoebelen |
16:00 - 16:30 | Symbolic Model Checking for
Probabilistic Timed Automata Marta Kwiatkowska, Gethin Norman, Jeremy Sproston and Fuzhi Wang |
||
| 11:45
- 12:15 |
Mixed delay and threshold
voters in
critical real-time systems Chiheb Kossentini and Paul Caspi |
16:30 - 17:00 | Structured Modeling of
Concurrent
Stochastic Hybrid Systems Mikhail Bernadskiy Raman Sharykin Rajeev Alur |
||
| Conference Dinner |
|||||
Friday September 24, 2004 |
|||||
Morning |
Afternoon |
||||
|
9:30 - 10:30 |
|
14:00
- 14:30 |
Computing Schedules for
Multithreaded
Real-Time Programs using Geometry Philippe Gerner and Thao Dang |
||
| 10:30 - 10:45 | Coffee break | 14:30
- 15:00 |
Forward Reachability
Analysis of Timed
Petri Nets Parosh Abdulla, Johann Deneux, Pritha Mahata and Aletta Nylen |
||
| 10:45 - 11:15 | Robustness and
Implementability of Timed Automata Martin De Wulf, Laurent Doyen, Nicolas Markey and Jean-Francois Raskin |
15:30
- 16:00 |
Lazy Approximation for
Dense Real-Time
Systems Maria Sorea |
||
| 11:15 - 11:45 | Real-time Testing with
Timed Automata Testers and Coverage Criteria Moez Krichen and Stavros Tripakis |
16:00 - 16:30 | Learning of Event-Recording
Automata Olga Grinchtein, Bengt Jonsson, Martin Leucker |
||
| 11:45 - 12:15 | Monitoring Temporal
Properties of Continuous Signals Oded Maler and Dejan Nickovic |
||||