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 shows that by judiciously abstracting away extraneous complexity, the state space of the model could be exhaustively searched allowing critical functional requirement to be validated down to the design level.


    Access

    Access via TIB

    Check availability in my library


    Export, share and cite



    Title :

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


    Contributors:
    Schneider, F. (author) / Easterbrook, S. (author) / Callahan, J. (author) / Holzmann, G. (author) / Reinholtz, W. (author) / Ko, A. (author) / Shahabuddin, M. (author)


    Publication date :

    1999-02-01


    Type of media :

    Miscellaneous


    Type of material :

    No indication


    Language :

    English




    Validating Requirements for Fault Tolerant Systems Using Model Checking

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


    Validating requirements for fault tolerant systems using model checking

    Schneider, F. / Easterbrook, S.M. / Callahan, J.R. et al. | Tema Archive | 1998



    Verifying and validating a land use — transport — environment model

    Gu, Kevin / Young, William | Taylor & Francis Verlag | 1998


    A Structured Approach to Verifying and Validating Expert Systems

    McAlindon, P. J. / Gupta, U. G. | British Library Conference Proceedings | 1993