Anzeige
Erschienen in:
2009 | OriginalPaper | Buchkapitel
A Formal Method for Developing Provably Correct Fault-Tolerant Systems Using Partial Refinement and Composition
verfasst von : Ralph Jeffords, Constance Heitmeyer, Myla Archer, Elizabeth Leonard
Erschienen in: FM 2009: Formal Methods
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.