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. Section 1 gives an informal account of real-time systems. Section 2.1 presents a historic background on formal techniques in real-time and fault-tolerance. Section 2.2 gives an outline of the approach used in this chapter. Section 3 introduces the computational model and the Temporal Logic of Actions [144] used for program specification, verification and refinement. In Section 4, we show how physical faults are specified, how fault-tolerance is achieved by transforming a non-fault-tolerant program, and how fault-tolerance is verified and refined. Section 5 extends the method given in Section 3 for the specification and verification of real-time programs. In Section 6 we combine the techniques used for fault-tolerance and real-time. Section 7 shows how real-time scheduling policies can be specified and combined with the program specification for verification of schedulability of a program. Proof rules for feasibility and fault-tolerant feasibility are also developed and it is shown how methods and results from scheduling theory can be formally verified and used. The notation, model and techniques are illustrated using a simple processor-memory interface program. © Springer-Verlag Berlin Heidelberg 2006.