Stepwise development of fault-tolerant reactive systems

Abstract

Consider a reactive system of the form S1 || S2. Given the specification of one component, say S1, methods are available to design S2 in a stepwise manner such that the composed system S1 || S2 satisfies a given specification. In this paper, we use a similar paradigm to construct a fault-tolerant program. Given a program S1 that may suffer from hardware faults or software design faults, we show how a stepwise method can be used to design a program S2 so that S1 || S2 meets a given specification. The main idea is demonstrated by solving a resource allocation problem.