Formal Techniques in Real-Time and Fault-Tolerant Systems

1. Front Matter

   PDF

2. ISL: An interval logic for the specification of real-time programs

   • Asis Goswami, Michael Bell, Mathai Joseph

   Pages 1-20

3. Duration specifications for shared processors

   • Zhou Chaochen, Michael R. Hansen, Anders P. Ravn, Hans Rischel

   Pages 21-32

4. A compositional semantics for fault-tolerant real-time systems

   • J. Coenen, J. Hooman

   Pages 33-51

5. Modelling real-time behavior with an interval time calculus

   • Mats Daniels

   Pages 53-71

6. Multicycles and RTL logic satisfiability

   • Odile Millet

   Pages 73-86

7. Voluntary preemption: A tool in the design of hard real-time systems

   • Abha Moitra

   Pages 87-106

8. Observing task preemption in Ada 9X

   • K. T. Narayana

   Pages 107-129

9. Real-time scheduling by queue automata

   • L. Breveglieri, A. Cherubini, S. Crespi-Reghizzi

   Pages 131-147

10. Broadcast communication for real-time processes

    • Jim Davies, Dave Jackson, Steve Schneider

    Pages 149-169

11. Analysis of timeliness requirements in safety-critical systems

    • Rogério de Lemos, Amer Saeed, Tom Anderson

    Pages 171-192

12. Verification of a reliable net protocol

    • Victor Yodaiken, Krithi Ramamritham

    Pages 193-215

13. Mechanical verification of a generalized protocol for Byzantine fault tolerant clock synchronization

    • Natarajan Shankar

    Pages 217-236

14. Formal specification and verification of a fault-masking and transient-recovery model for digital flight-control systems

    • John Rushby

    Pages 237-257

15. On fault-tolerant symbolic computations

    • Bernard Delyon, Oded Maler

    Pages 259-269

16. Temporal logic applied to reliability modelling of fault-tolerant systems

    • Klaus D. Heidtmann

    Pages 271-289

17. Specifying asynchronous transfer of control

    • Padmanabhan Krishnan, Peter D. Mosses

    Pages 291-306

18. Protocol design by layered decomposition

    • Wil Janssen, Job Zwiers

    Pages 307-326

19. Scheduling in Real-Time Models

    • Reino Kurki-Suonio, Kari Systä, Jüri Vain

    Pages 327-339

20. A temporal approach to requirements specification of real-time systems

    • Yogesh Naik

    Pages 341-361

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.

• formal logic
• formal method
• logic
• real-time
• semantics
• system
• verification

Policies and ethics