Name
Title | ||
|---|---|---|
Model-based construction and verification of critical systems using composition and partial refinement |
Abstract | ||
|---|---|---|
This article introduces a new model-based method for incrementally constructing critical systems and illustrates its application to the development of fault-tolerant systems. The method relies on a special form of composition to combine software components and a set of proof rules to obtain high confidence of the correctness of the composed system. As in conventional component-based software development, two (or more) components are combined, but in contrast to many component-based approaches used in practice, which combine components consisting of code, our method combines components represented as state machine models. In the first phase of the method, a model is developed of the normal system behavior, and system properties are shown to hold in the model. In the second phase, a model of the required fault-handling behavior is developed and "or-composed" with the original system model to create a fault-tolerant extension which is, by construction, "fully faithful" (every execution possible in the normal system is possible in the fault-tolerant system). To model the fault-handling behavior, the set of states of the normal system model is extended through new state variables and new ranges for some existing state variables, and new fault-handling transitions are defined. Once constructed, the fault-tolerant extension is shown, using a set of property inheritance and compositional proof rules, to satisfy both the overall system properties, typically weakened, and selected fault-tolerance properties. These rules can often be used to verify the properties automatically. To provide a formal foundation for the method, formal notions of or-composition, partial refinement, fault-tolerant extension, and full faithfulness are introduced. To demonstrate and validate the method, we describe its application to a real-world, fault-tolerant avionics system. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/s10703-010-0106-9 | Formal Methods in System Design |
Keywords | Field | DocType |
Formal specification,Refinement,Composition,Proof rules,Fault-tolerance,Theorem proving,Masking | Computer science,Correctness,Automated theorem proving,Algorithm,Formal specification,Finite-state machine,Theoretical computer science,State variable,Component-based software engineering,Software development,System model | Journal |
Volume | Issue | ISSN |
37 | 2-3 | 0925-9856 |
Citations | PageRank | References |
4 | 0.40 | 27 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ralph D. Jeffords | 1 | 434 | 34.88 |
| Constance L. Heitmeyer | 2 | 898 | 151.71 |
| Myla M. Archer | 3 | 11 | 1.29 |
| Elizabeth I. Leonard | 4 | 110 | 8.48 |