Dynamic scheduling and fault-tolerance: Specification and verification

Consider a distributed real-time program which is executed on a system with a limited set of hardware resources. Assume the program is required to satisfy some timing constraints, despite the occurrence of anticipated hardware failures. For efficient use of resources, scheduling decisions must be taken at run-time, considering deadlines, the load and hardware failures. The paper demonstrates how to reason about such dynamically scheduled programs in the framework of a timed process algebra and modal logic. The algebra provides a uniform process encoding of programs, hardware and schedulers, with an operational semantics of a process depending on the assumptions about faults. The logic specifies the timing properties of a process and verifies them via this fault-affected semantics, establishing fault-tolerance. The approach lends itself to application of existing tools and results supporting reasoning in process algebras and modal logics.