A formal method for developing provably correct fault-tolerant systems using partial refinement and composition

Abstract

It is widely agreed that building correct fault-tolerant systems is very difficult. To address this problem, this paper introduces a new model-based approach for developing masking fault-tolerant systems. As in component-based software development, two (or more) component specifications are developed, one implementing the required normal behavior and the other(s) the required fault-handling behavior. The specification of the required normal behavior is verified to satisfy system properties, whereas each specification of the required fault-handling behavior is shown to satisfy both system properties, typically weakened, and fault-tolerance properties, both of which can then be inferred of the composed fault-tolerant system. The paper presents the formal foundations of our approach, including a new notion of partial refinement and two compositional proof rules. To demonstrate and validate the approach, the paper applies it to a real-world avionics example. © 2009 Springer-Verlag Berlin Heidelberg.