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.
Author(s): N. Halbwachs, J. -F. Héry, J. -C. Laleuf, X. Nicollin (auth.), Mathai Joseph (eds.)
Series: Lecture Notes in Computer Science 1926
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2000
Language: English
Pages: 314
Tags: Logics and Meanings of Programs; Programming Languages, Compilers, Interpreters; Processor Architectures; Special Purpose and Application-Based Systems; Logic Design
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
