Formal Techniques in Real-Time and Fault-Tolerant Systems: 6th International Symposium, FTRTFT 2000 Pune, India, September 20-22, 2000 Proceedings

Front Cover
Mathai Joseph
Springer Science & Business Media, Sep 6, 2000 - Computers - 314 pages
The six Schools and Symposia on Formal Techniques in Real Time and Fault Tolerant Systems (FTRTFT) have seen the eld develop from tentative explo- tions to a far higher degree of maturity, and from being under the scrutiny of a few interested software designers and academics to becoming a well-established area of inquiry. A number of new topics, such as hybrid systems, have been g- minated at these meetings and cross-links explored with related subjects such as scheduling theory. There has certainly been progress during these 12 years, but it is sobering to see how far and how fast practice has moved ahead in the same time, and how much more work remains to be done before the design of a mission-critical system can be based entirely on sound engineering principles underpinned by solid scienti c theory. The Sixth School and Symposium were organized by the Tata Research - velopment and Design Centre in Pune, India. The lectures at the School were given by Ian Hayes (U. of Queensland), Paritosh Pandya (Tata Institute of F- damental Research), Willem-Paul de Roever (Christian Albrechts U. ) and Joseph Sifakis (VERIMAG). There were three invited lectures at the Symposium, by Werner Damm (U. of Oldenburg), Nicholas Halbwachs (VERIMAG) and Yoram Moses (Technion). A sizable number of submissions were received for the Symposium from a- hors representing 16 di erent countries.
 

Contents

Stability of Discrete Sampled Systems
1
Issues in the Refinement of Distributed Programs Invited Talk
12
Challenges in the Verification of Electronic Control Units
18
Scaling up Uppaal Automatic Verification of RealTime Systems using Compositionality and Abstraction
19
Decidable Model Checking of Probabilistic Hybrid Automata
31
InvariantBased Synthesis of FaultTolerant Systems
46
Modeling Faults of Distributed Reactive Systems
58
Threshold and BoundedDelay Voting in Critical Control Systems
70
A System for Object Code Validation
152
RealTime Program Refinement Using Auxiliary Variables
170
On Refinement and Temporal Annotations
185
Generalizing Action Systems to Hybrid Systems
202
Compositional Verification of Synchronous Networks
214
Modelling Coordinated Atomic Actions in Timed CSP
228
A Logical Characterisation of Event Recording
240
Using Cylindrical Algebraic Decomposition for the Analysis of Slope Parametric Hybrid Automata
252

Automating the Addition of FaultTolerance
82
Reliability Modelling of TimeCritical Distributed Systems
94
A Methodology for the Construction of Scheduled Systems
106
A Dual Interpretation of Standard Constraints in Parametric Scheduling
121
SignalSimulink
134
Probabilistic Neighbourhood Logic
264
An OntheFly Tableau Construction for a RealTime Temporal Logic
276
Verifying Universal Properties of Parameterized Networks
291
Author Index
304
Copyright

Other editions - View all

Common terms and phrases

Bibliographic information