| Systems in which the consequences of failure are very serious or life-threatening are generally called safety critical. These systems exist in many facets of everyday life; transportation systems, environmental protection, aerospace, medicine and power generation. The correct and safe operation of these systems depends largely on the hardware and software architecture, and the underlying principles of those architectures. The software and hardware in these systems are usually substantial and complex.; Recently, an approach called runtime verification has been gaining support because it attempts to not only detect and/or correct the effects of faults as traditional fault tolerance schemes do, but it additionally verifies the correct operation of the executing software. In essence, runtime verification makes use of a monitor that checks the behavior of the computing platform with respect to some reference of acceptable behavior. To date, a sound theory (in the way of design properties and checking conditions) integrating safety critical system design and runtime verification design has not been explored thoroughly.; To address this deficiency, a theory of runtime verification for safety critical systems is developed and described in this dissertation. Specific contributions presented in this dissertation are: (1) The development of theory that will allow designers of runtime verification systems to formally assess design assumptions and capabilities of particular runtime architecture for safety critical systems. The approach developed allows a wide and range runtime verification schemes to be characterized on properties they should have, irrespective of their implementation details. Specifically, the theory builds on formal descriptions of computations of reactive systems (o-automata) and properties of executions (safety properties). The theory introduces and defines the notion of completeness, accuracy, and soundness properties for safety monitors, and defines those properties in relation to fault classes. Furthermore, the theory separates properties of the target computer execution (safety) from the properties of the safety monitor, extending earlier work on safety kernels. (2) Using properties to describe the behavior of safety monitors allows one to classify safety monitors according to their composition of properties that they have. This property-based approach is a bridge between the implementation-oriented models of runtime verification and the conceptual characterizations of runtime verifications. |
