Formal Techniques in Real-Time and Fault-Tolerant Systems: 6th International Symposium, FTRTFT 2000 Pune, India, September 20-22, 2000 Proceedings (Lecture Notes in Computer Science (1926))

This book constitutes the refereed proceedings of the 6th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2000, held in Pune, India in September 2000. The 21 revised full papers presented together with three invited contributions were carefully reviewed and selected from numerous submissions. The papers are organized in topical sections on model checking, fault tolerance, scheduling, validation, verification, logic and automata. Stability of Discrete Sampled Systems....Pages 1-11 Issues in the Refinement of Distributed Programs....Pages 12-17 Challenges in the Verification of Electronic Control Units....Pages 18-18 Scaling up Uppaal....Pages 19-30 Decidable Model Checking of Probabilistic Hybrid Automata....Pages 31-45 Invariant-Based Synthesis of Fault-Tolerant Systems....Pages 46-57 Modeling Faults of Distributed, Reactive Systems....Pages 58-69 Threshold and Bounded-Delay Voting in Critical Control Systems....Pages 70-81 Automating the Addition of Fault-Tolerance....Pages 82-93 Reliability Modelling of Time-Critical Distributed Systems....Pages 94-105 A Methodology for the Construction of Scheduled Systems....Pages 106-120 A Dual Interpretation of “Standard Constraints” in Parametric Scheduling....Pages 121-133 Co-Simulation of Hybrid Systems: Signal-Simulink....Pages 134-151 A System for Object Code Validation....Pages 152-169 Real-Time Program Refinement Using Auxiliary Variables....Pages 170-184 On Refinement and Temporal Annotations....Pages 185-202 Generalizing Action Systems to Hybrid Systems....Pages 202-213 Compositional Verification of Synchronous Networks....Pages 214-227 Modelling Coordinated Atomic Actions in Timed CSP....Pages 228-239 A Logical Characterisation of Event Recording Automata....Pages 240-251 Using Cylindrical Algebraic Decomposition for the Analysis of Slope Parametric Hybrid Automata....Pages 252-263 Probabilistic Neighbourhood Logic....Pages 264-275 An On-the-Fly Tableau Construction for a Real-Time Temporal Logic....Pages 276-290 Verifying Universal Properties of Parameterized Networks....Pages 291-303 Formal Techniques in Real-Time and Fault-Tolerant Systems: 6th International Symposium,FTRTFT 2000 Pune, India, September 20–22, 2000 Proceedings Author: Mathai Joseph Published by Springer Berlin Heidelberg ISBN: 978-3-540-41055-3 DOI: 10.1007/3-540-45352-0 Table of Contents: Stability of Discrete Sampled Systems Issues in the Refinement of Distributed Programs Challenges in the Verification of Electronic Control Units Scaling up Uppaal Decidable Model Checking of Probabilistic Hybrid Automata Invariant-Based Synthesis of Fault-Tolerant Systems Modeling Faults of Distributed, Reactive Systems Threshold and Bounded-Delay Voting in Critical Control Systems Automating the Addition of Fault-Tolerance Reliability Modelling of Time-Critical Distributed Systems A Methodology for the Construction of Scheduled Systems A Dual Interpretation of “Standard Constraints” in Parametric Scheduling Co-Simulation of Hybrid Systems: Signal-Simulink A System for Object Code Validation Real-Time Program Refinement Using Auxiliary Variables On Refinement and Temporal Annotations Generalizing Action Systems to Hybrid Systems Compositional Verification of Synchronous Networks Modelling Coordinated Atomic Actions in Timed CSP A Logical Characterisation of Event Recording Automata Many real-time embedded systems, appearing in industrial control (e.g., plant supervision, flight control, ... ), are periodic sampled systems.