Safety, Liveness, and Information Flow: Dependability Revisited

Abstract: We present a formal framework to talk and reason about dependable systems. The framework is based on three distinct classes of (system specification) properties we call safety, liveness and information flow. We discuss several examples of dependable systems within this framework and argue that these classes are sufficient to model the functional requirements of dependable systems satisfying to high degrees both fault-tolerance and security attributes. The framework is meant to be a minimal security-specific extension of the asynchronous system model from fault-tolerant distributed algorithms and aimed to support teaching the concepts of fault-tolerance and security within a uniform system model. To remain minimal, the framework does not cover probabilistic or complexity theoretic aspects of dependability (like reliability or computational security).

• Type: Conference
• Year: 2006
• Where: ARCS
• Authors: Zinaida Benenson, Felix C. Freiling, Thorsten Holz, Dogan Kesdogan, Lucia Draque Penso
• Keywords: ARCS 2006, Dependable Systems, Formal Framework, Minimal Security-specific Extension, Software Engineering