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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 2009
- Accession Number
- ADA631287
Entities
People
- Constance Heitmeyer
- Elizabeth Leonard
- Myla M. Archer
- Ralph Jeffords
Organizations
- United States Naval Research Laboratory