Real-Time and Fault-Tolerant Systems

Abstract

In this chapter, we show that functional and many non-functional properties of a real-time system, such as schedulability, or proving that its implementation meets its timing constraints, can be verified in a similar way. Likewise, the fault-tolerance of a system can be proved using the same techniques. We use a single notation and model and take a unified view of the functional and non-functional properties of programs. A simple transformational method is used to combine these properties [167, 168]. We show how the theory of concurrency, fault-tolerance, real-time and scheduling can be built on the theories of sequential programming, such as those of Dijkstra’s calculus of weakest preconditions [81], Hoare Logic [114], Morgan’s refinement calculus [192] and Hoare and He’s UTP [117]. These theories are discussed and used in Chapter 4 and Chapter 6.