Model checking is shown to be an effective tool in validating the behavior of a fault tolerant embedded spacecraft controller. The case study presented, shows that by judiciously abstracting away extraneous complexity, the state space of the model could be exhaustively searched allowing critical functional requirements to be validated 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.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Validating requirements for fault tolerant systems using model checking


    Contributors:


    Publication date :

    1998


    Size :

    10 Seiten, 14 Quellen




    Type of media :

    Conference paper


    Type of material :

    Print


    Language :

    English




    Validating Requirements for Fault Tolerant Systems Using Model Checking

    Holzlmann, Gerard J. / Callahan, John R. / Easterbrook, Steve M. et al. | NTRS | 1998


    A Process for Verifying and Validating Requirements for Fault Tolerant Systems Using Model Checking

    Schneider, F. / Easterbrook, S. / Callahan, J. et al. | NTRS | 1999


    REFERENCE TRAJECTORY VALIDATING AND COLLISION CHECKING MANAGEMENT

    CLAWSON TAYLOR SCOTT / TOUPET OLIVIER AMAURY | European Patent Office | 2024

    Free access

    REFERENCE TRAJECTORY VALIDATING AND COLLISION CHECKING MANAGEMENT

    CLAWSON TAYLOR SCOTT / TOUPET OLIVIER AMAURY | European Patent Office | 2025

    Free access

    REFERENCE TRAJECTORY VALIDATING AND COLLISION CHECKING MANAGEMENT

    CLAWSON TAYLOR SCOTT / TOUPET OLIVIER AMAURY | European Patent Office | 2024

    Free access