Formal Techniques In Real-time And Fault-tolerant Systems: Second International Symposium, Nijmegen, The Netherlands, January 8-10, 1992. Proceedings (lecture Notes In Computer Science)

This book presents state-of-the-art research results in the area of formal methods for real-time and fault-tolerant systems. The papers consider problems and solutions in safety-critical system design and examine how wellthe use of formal techniques for design, analysis and verification serves in relating theory to practical realities. The book contains papers on real-time and fault-tolerance issues. Formal logic, process algebra, and action/event models are applied: - to specify and model qualitative and quantitative real-time and fault-tolerant behavior, - to analyze timeliness requirements and consequences of faulthypotheses, - to verify protocols and program code, - to formulate formal frameworks for development of real-time and fault-tolerant systems, - to formulate semantics of languages. The integration and cross-fertilization of real-time and fault-tolerance issues have brought newinsights in recent years, and these are presented in this book. ISL: An interval logic for the specification of real-time programs....Pages 1-20 Duration specifications for shared processors....Pages 21-32 A compositional semantics for fault-tolerant real-time systems....Pages 33-51 Modelling real-time behavior with an interval time calculus....Pages 53-71 Multicycles and RTL logic satisfiability....Pages 73-86 Voluntary preemption: A tool in the design of hard real-time systems....Pages 87-106 Observing task preemption in Ada 9X....Pages 107-129 Real-time scheduling by queue automata....Pages 131-147 Broadcast communication for real-time processes....Pages 149-169 Analysis of timeliness requirements in safety-critical systems....Pages 171-192 Verification of a reliable net protocol....Pages 193-215 Mechanical verification of a generalized protocol for Byzantine fault tolerant clock synchronization....Pages 217-236 Formal specification and verification of a fault-masking and transient-recovery model for digital flight-control systems....Pages 237-257 On fault-tolerant symbolic computations....Pages 259-269 Temporal logic applied to reliability modelling of fault-tolerant systems....Pages 271-289 Specifying asynchronous transfer of control....Pages 291-306 Protocol design by layered decomposition....Pages 307-326 Scheduling in Real-Time Models....Pages 327-339 A temporal approach to requirements specification of real-time systems....Pages 341-361 RLucid, a general real-time dataflow language....Pages 363-374 A mechanized theory for the verification of real-time program code using higher order logic....Pages 375-392 Specification and verification of real-time behaviour using Z and RTL....Pages 393-409 TAM: A formal framework for the development of distributed real-time systems....Pages 411-428 An attempt to confront asynchronous reality to synchronous modelization in the ESTEREL language....Pages 429-450 The real-time behaviour of asynchronously communicating processes....Pages 451-472 Asynchronous communication in real space process algebra....Pages 473-492 Translating timed process algebra into prioritized process algebra....Pages 493-506 Operational semantics for timed observations....Pages 507-527 Real-timed concurrent refineable behaviours....Pages 529-545 Stepwise development of model-oriented real-time specifications from action/event models....Pages 547-570 Formal specification of fault tolerant real time systems using minimal 3-sorted modal logic....Pages 571-590 Timed and Hybrid Statecharts and their textual representation....Pages 591-620

This book presents state-of-the-art research results in the area of formal methods for real-time and fault-tolerant systems. The papers consider problems and solutions in safety-critical system design and examine how wellthe use of formal techniques for design, analysis and verification serves in relating theory to practical realities.
The book contains papers on real-time and fault-tolerance issues. Formal logic, process algebra, and action/event models are applied:
- to specify and model qualitative and quantitative real-time and fault-tolerant behavior,
- to analyze timeliness requirements and consequences of faulthypotheses,
- to verify prools and program code,
- to formulate formal frameworks for development of real-time and fault-tolerant systems,
- to formulate semantics of languages.
The integration and cross-fertilization of real-time and fault-tolerance issues have brought newinsights in recent years, and these are presented in this book.

Presents research results on problems and solutions in safety-critical system design. This work applies logic, process algebra, and action/event models to specification, modeling, analysis and verification of real-time and fault-tolerant systems. Real-time systems are reactive systems [HP85, Pnu86] which must satisfy timing properties.