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 qu estion of determining whether a real-time program will meet its deadlines, i.e., showing that there is a feasible schedule, is usually done using sche duling theory, quite separately from the verification of other properties o f the program. This makes it hard to use the results of scheduling analysis in the design, or redesign, of fault-tolerant and real-time programs. This article shows how fault-tolerance, timing, and schedulability can be speci fied and verified using a single notation and model. This allows a unified view to be taken of the functional and nonfunctional properties of programs and a simple transformational method to be used to combine these propertie s. It also permits results from scheduling theory to be interpreted and use d within a formal proof framework. The notation and model are illustrated u sing a simple example.