TitleA Formal Method for Developing Provably Correct Fault-Tolerant Systems Using Partial Refinement and Composition
Publication TypeConference Proceedings
Year of Publication2009
AuthorsJeffords, R., C. L. Heitmeyer, M. Archer, and E. Leonard
Conference NameFormal Methods, Second World Congress (FM 2009)
Pagination173-189
Conference LocationEindhoven, The Netherlands
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 faulthandling 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.

Full Text

Jeffords etal2009.pdf

NRL Publication Release Number

09-1226-3133