Deontic Action Logics for Specification and Analysis of Fault-Tolerance

Abstract

<p> In this thesis we develop a mathematical framework to express and reason about properties of fault-tolerant computing systems. The main idea behind this mathematical framework is to use axiomatic theories to specify systems. The standard logical operators allow us to describe the basic behavior of the system, while we use deontic predicates on actions to express prescriptions about the system's behavior. 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. We develop our own deontic logic, keeping in mind that we want to use it for specifying fault-tolerant systems. We investigate the properties of this logic, commenting on those that are relevant to the use of the logic in practice. We provide two different deductive systems; one of them is a standard (Hilbert style) deductive system, while the other one is a tableaux system, which can be applied automatically to prove properties of specifications.</p> <p> In any specification language, it is important to have at hand mechanisms which enable designers to modularize the system description; we investigate how to apply these mechanisms to the logics proposed in this thesis, and, in particular, we focus on how the modularization of specifications affects the local prescriptions of a module (or component). We study the problems that arise from the interaction between components. We show that, in some cases, we can guarantee that the locality of violations in a particular component is preserved. Some examples are provided throughout this thesis to illustrate how the ideas described below can be applied in practice. </p>