2. FORMATS / 8. FTRTFT 2004: Grenoble, France

Invited Papers

• Paul Feautrier:
  From Software to Hardware and Back. 1-2
  
• Peter Y. A. Ryan:
  Of Elections and Electrons. 3-4
  

Regular Papers

• Samar Dajani-Brown, Darren D. Cofer, Amar Bouali:
  Formal Verification of an Avionics Sensor Voter Using SCADE. 5-20
  
• Chiheb Kossentini, Paul Caspi:
  Mixed Delay and Threshold Voters in Critical Real-Time Systems. 21-35
  
• Simona Bernardi, Susanna Donatelli, Giovanna Dondossola:
  Towards a Methodological Approach to Specification and Analysis of Dependable Automation Systems. 36-51
  
• Jennifer M. Davoren, Thomas Moor, Rajeev Goré, Vaughan Coulthard, Anil Nerode:
  On Two-Sided Approximate Model-Checking: Problem Formulation and Solution via Finite Topologies. 52-67
  
• Deepak D'Souza, Nicolas Tabareau:
  On Timed Automata with Input-Determined Guards. 68-83
  
• Dilsun Kirli Kaynar, Nancy A. Lynch:
  Decomposing Verification of Timed I/O Automata. 84-101
  
• Nicolas Markey, Ph. Schnoebelen:
  Symbolic Model Checking for Simply-Timed Systems. 102-117
  
• Martin De Wulf, Laurent Doyen, Nicolas Markey, Jean-François Raskin:
  Robustness and Implementability of Timed Automata. 118-133
  
• Moez Krichen, Stavros Tripakis:
  Real-Time Testing with Timed Automata Testers and Coverage Criteria. 134-151
  
• Oded Maler, Dejan Nickovic:
  Monitoring Temporal Properties of Continuous Signals. 152-166
  
• Paul S. Miner, Alfons Geser, Lee Pike, Jeffrey Maddalon:
  A Unified Fault-Tolerance Protocol. 167-182
  
• Felix C. Gärtner, Arshad Jhumka:
  Automating the Addition of Fail-Safe Fault-Tolerance: Beyond Fusion-Closed Specifications. 183-198
  
• Bruno Dutertre, Maria Sorea:
  Modeling and Verification of a Fault-Tolerant Real-Time Startup Protocol Using Calendar Automata. 199-214
  
• Catalin Dima, Alain Girault, Yves Sorel:
  Static Fault-Tolerant Real-Time Scheduling with "Pseudo-topological" Orders. 215-230
  
• Harald Fecher:
  The Influence of Durational Actions on Time Equivalences. 231-245
  
• Fang Yu, Bow-Yaw Wang, Yao-Wen Huang:
  Bounded Model Checking for Region Automata. 246-262
  
• Scott Cotton, Eugene Asarin, Oded Maler, Peter Niebert:
  Some Progress in Satisfiability Checking for Difference Logic. 263-276
  
• Thomas Brihaye, Véronique Bruyère, Jean-François Raskin:
  Model-Checking for Weighted Timed Automata. 277-292
  
• Marta Z. Kwiatkowska, Gethin Norman, Jeremy Sproston, Fuzhi Wang:
  Symbolic Model Checking for Probabilistic Timed Automata. 293-308
  
• Mikhail Bernadsky, Raman Sharykin, Rajeev Alur:
  Structured Modeling of Concurrent Stochastic Hybrid Systems. 309-324
  
• Philippe Gerner, Thao Dang:
  Computing Schedules for Multithreaded Real-Time Programs Using Geometry. 325-342
  
• Parosh Aziz Abdulla, Johann Deneux, Pritha Mahata, Aletta Nylén:
  Forward Reachability Analysis of Timed Petri Nets. 343-362
  
• Maria Sorea:
  Lazy Approximation for Dense Real-Time Systems. 363-378
  
• Olga Grinchtein, Bengt Jonsson, Martin Leucker:
  Learning of Event-Recording Automata. 379-396