Synthesizing Fault-Tolerant Programs from Deontic Logic Specifications

Abstract

This dissertation concentrates on 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 fragment of a branching time temporal logic with deontic operators, especially designed for fault-tolerant component specification. Deontic logics have proved to be useful for reasoning about legal and moral systems, where the situation is more or less similar to fault-tolerance: there exists a set of rules that states what the normal behaviours or scenarios are. Violations arise when these rules are not followed and, as a consequence, some actions must be performed to return to a normal or desirable state. As a black-box overview, our synthesis algorithm takes the component specification and a user-defined level of fault-tolerance (masking, nonmasking, or 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. Some case studies are provided throughout this thesis to illustrate how the ideas described below can be applied in practice. Moreover, we have implemented a tool called dCTL Synthesizer (syntdctl) which was used to synthesize automatically well-known fault-tolerant examples.