Specification and Verification of Fault-tolerance, Timing and Scheduling

Fault-tolerance and timing have often been considered to be implementation issues of a program, quite distinct from the functional safety and liveness properties. Recent work has shown how these non-functional and functional properties can be verified in a similar way. However, the more practical question of determining whether a real-time program will meet its deadlines, i.e. showing that there is a feasible schedule, is usually done using scheduling theory, quite separately from the verification of other properties of the program. This makes it hard to use the results of scheduling analysis in the design, or re-design, of fault-tolerant, real-time programs. This paper shows how fault-tolerance, timing and schedulability can be specified and verified using a single notation and model. This allows a unified view to be taken of the functional and non-functional properties of programs and a simple transformational method to be used to combine these properties. It also permits results fro..