syntMaskFT: A Tool for Synthesizing Masking Fault-Tolerant Programs from Deontic Specifications

Abstract

In this paper we introduce syntMaskFT, a tool that synthe- sizes fault-tolerant programs from specifications written in a fragment of branching time logic with deontic operators, designed for specifying fault-tolerant systems. The tool focuses on producing masking tolerant programs, that is, programs that during a failure mask faults in such a way that they cannot be observed by the environment. It is based on an algorithm we have introduced in previous work, and shown to be sound and complete. syntMaskFT takes a specification and automatically deter- mines whether a masking fault-tolerant component is realizable; in such a case, a description of the component is produced together with the maximal set of faults that can be supported for this level of tolerance. We present the ideas behind the tool by means of a simple example, and also report the result of experiments realized with more complex case studies.