Synthesizing fault-tolerant programs from deontic logic specifications

Abstract

We study the problem of synthesizing fault-tolerant components from specifications, i.e., the problem of automatically constructing a fault-tolerant component implementation from a logical specification of the component, and the system's required level of fault-tolerance. In our approach, the logical specification of the component is given in dCTL, a branching time temporal logic with deontic operators, especially designed for fault-tolerant component specification. The synthesis algorithm takes the component specification, and a user-defined level of fault-tolerance (masking, nonmasking, failsafe), and automatically determines whether a component with the required fault-tolerance is realizable. Moreover, if the answer is positive, then the algorithm produces such a fault-tolerant implementation. Our technique for synthesis is based on the use of (bi)simulation algorithms for capturing different fault-tolerance classes, and the extension of a synthesis algorithm for CTL to cope with dCTL specifications.