Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems: Joint International Conferences on Formal Modeling and Analysis of Timed Systmes, FORMATS 2004, and Formal Techniques in Real-Time and Fault -Tolerant Systems, FTRTFT 2004, Gre

This book constitutes the refereed proceedings of the joint International Conferences Formal Modeling and Analysis of Timed Systems, FORMATS 2004, and Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2004, held in Grenoble, France, in September 2004. The 24 revised full papers presented together with abstracts of 2 invited talks were carefully reviewed and selected from 70 submissions. Among the topics addressed are formal verification, voting systems, formal specification, dependable automation systems, model checking, timed automata, real-time testing, fault-tolerance protocols, fail-safe fault tolerance, real-time scheduling, satisfiability checking, symbolic model checking, stochastic hybrid systems, timed Petri nets, and event recording automata. This Volume Contains The Proceedings Of The Joint Conference On Formal M- Elling And Analysis Of Timed Systems (formats) And Formal Techniques In Real-time And Fault Tolerant Systems (ftrtft), Held In Grenoble,france,on September 22–24,2004. The Conference United Two Previously Independently - Ganized Conferences Formats And Ftrtft. Formats 2003 Was Organized Asasatelliteworkshopofconcur2003andwasrelatedtothreeindependently Started Workshop Series: Mtcs (held As A Satellite Event Of Concur 2000 And Concur 2002), Rt-tools (held As A Satellite Event Of Concur 2001 And Floc 2002) And Tpts (held At Etaps 2002). Ftrtft Is A Symposium That Was Held Seven Times Before: In Warwick 1988, Nijmegen 1992, Lu ̈beck 1994, Uppsala 1996, Lyngby 1998, Pune 2000 And Oldenburg 2002. The Proceedings Of These Symposia Were Published As Volumes 331, 571, 863, 1135, 1486, 1926, And 2469 In The Lncs Series By Springer. Thisjointconferenceis Dedicatedtotheadvancementofthetheoryandpr- Ticeofthe Modelling,designandanalysisofreal-timeandfault-tolerantsystems. Indeed,computersystemsarebecomingincreasinglywidespreadinreal-timeand Safety-critical Applications Such As Embedded Systems. Such Systems Are Char- Terized By The Crucial Need To Manage Their Complexity In Order To Produce Reliable Designs And Implementations. The Importance Of Timing Aspects, P- Formance And Fault-tolerance Is Continuously Growing. Formal Techniques O?er A Foundation For Systematic Design Of Complex Systems. They Have Bene?cial - Plications Throughout The Engineering Process, From The Capture Of Requirements Through Speci?cation, Design, Coding And Compilation, Down To The Hardware That Embeds The System Into Its Environment. Invited Papers -- From Software To Hardware And Back -- Of Elections And Electrons -- Regular Papers -- Formal Verification Of An Avionics Sensor Voter Using Scade -- Mixed Delay And Threshold Voters In Critical Real-time Systems -- Towards A Methodological Approach To Specification And Analysis Of Dependable Automation Systems -- On Two-sided Approximate Model-checking: Problem Formulation And Solution Via Finite Topologies -- On Timed Automata With Input-determined Guards -- Decomposing Verification Of Timed I/o Automata -- Symbolic Model Checking For Simply-timed Systems -- Robustness And Implementability Of Timed Automata -- Real-time Testing With Timed Automata Testers And Coverage Criteria -- Monitoring Temporal Properties Of Continuous Signals -- A Unified Fault-tolerance Protocol -- Automating The Addition Of Fail-safe Fault-tolerance: Beyond Fusion-closed Specifications -- Modeling And Verification Of A Fault-tolerant Real-time Startup Protocol Using Calendar Automata -- Static Fault-tolerant Real-time Scheduling With “pseudo-topological” Orders -- The Influence Of Durational Actions On Time Equivalences -- Bounded Model Checking For Region Automata -- Some Progress In Satisfiability Checking For Difference Logic -- Model-checking For Weighted Timed Automata -- Symbolic Model Checking For Probabilistic Timed Automata -- Structured Modeling Of Concurrent Stochastic Hybrid Systems -- Computing Schedules For Multithreaded Real-time Programs Using Geometry -- Forward Reachability Analysis Of Timed Petri Nets -- Lazy Approximation For Dense Real-time Systems -- Learning Of Event-recording Automata. Yassine Lakhnech, Sergio Yovine (eds.). Internat. Conference Proceedings. Includes Bibliographical References And Index. Front Matter....Pages - From Software to Hardware and Back....Pages 1-2 Of Elections and Electrons....Pages 3-4 Formal Verification of an Avionics Sensor Voter Using SCADE....Pages 5-20 Mixed Delay and Threshold Voters in Critical Real-Time Systems....Pages 21-35 Towards a Methodological Approach to Specification and Analysis of Dependable Automation Systems....Pages 36-51 On Two-Sided Approximate Model-Checking: Problem Formulation and Solution via Finite Topologies....Pages 52-67 On Timed Automata with Input-Determined Guards....Pages 68-83 Decomposing Verification of Timed I/O Automata....Pages 84-101 Symbolic Model Checking for Simply-Timed Systems....Pages 102-117 Robustness and Implementability of Timed Automata....Pages 118-133 Real-Time Testing with Timed Automata Testers and Coverage Criteria....Pages 134-151 Monitoring Temporal Properties of Continuous Signals....Pages 152-166 A Unified Fault-Tolerance Protocol....Pages 167-182 Automating the Addition of Fail-Safe Fault-Tolerance: Beyond Fusion-Closed Specifications....Pages 183-198 Modeling and Verification of a Fault-Tolerant Real-Time Startup Protocol Using Calendar Automata....Pages 199-214 Static Fault-Tolerant Real-Time Scheduling with “Pseudo-topological” Orders....Pages 215-230 The Influence of Durational Actions on Time Equivalences....Pages 231-245 Bounded Model Checking for Region Automata....Pages 246-262 Some Progress in Satisfiability Checking for Difference Logic....Pages 263-276 Model-Checking for Weighted Timed Automata....Pages 277-292 Symbolic Model Checking for Probabilistic Timed Automata....Pages 293-308 Structured Modeling of Concurrent Stochastic Hybrid Systems....Pages 309-324 Computing Schedules for Multithreaded Real-Time Programs Using Geometry....Pages 325-342 Forward Reachability Analysis of Timed Petri Nets....Pages 343-362 Lazy Approximation for Dense Real-Time Systems....Pages 363-378 Learning of Event-Recording Automata....Pages 379-395 Back Matter....Pages -