Sciweavers

ICRE
1998
IEEE

Validating Requirements for Fault Tolerant Systems using Model Checking

13 years 8 months ago
Validating Requirements for Fault Tolerant Systems using Model Checking
Model checking is shown to be an effective tool in validating the behavior of a fault tolerant embedded spacecraft controller. The case study presented here at by judiciously abstracting away extraneous complexity, the state space of the model could be exhaustively searched allowing critical functional requirements lidated down to the design level. Abstracting away detail not germane to the problem of interest leaves by definition a partial specification behind. The success of this procedure shows that it is feasible to effectively validate a partial specification with this technique. Three anomalies were found in the system. One was an error in the detailed requirements, and the other two were missing/ambiguous requirements. Because the method allows validation of partial specifications, it is also an effective approach for maintaining fidelity between a co-evolving specification and an implementation.
Francis Schneider, Steve M. Easterbrook, John R. C
Added 04 Aug 2010
Updated 04 Aug 2010
Type Conference
Year 1998
Where ICRE
Authors Francis Schneider, Steve M. Easterbrook, John R. Callahan, Gerard J. Holzmann
Comments (0)