Flight software is the central nervous system of modern spacecraft. Verifying spacecraft flight software to assure that it operates correctly and safely is presently an intensive and costly process. A multitude of scenarios and tests must be devised, executed and reviewed to provide reasonable confidence that the software will perform as intended and not endanger the spacecraft. Undetected software defects on spacecraft and launch vehicles have caused embarrassing and costly failures in recent years. Model checking is a technique for software verification that can detect concurrency defects that are otherwise difficult to discover. Within appropriate constraints, a model checker can perform an exhaustive state-space search on a software design or implementation and alert the implementing organization to potential design deficiencies. Unfortunately, model checking of large software systems requires an often-too-substantial effort in developing and maintaining the software functional models. A recent development in this area, however, promises to enable software-implementing organizations to take advantage of the usefulness of model checking without hand-built functional models. This development is the appearance of "model extractors". A model extractor permits the automated and repeated testing of code as built rather than of separate design models. This allows model checking to be used without the overhead and perils involved in maintaining separate models. We have attempted to apply model checking to legacy flight software from NASA's Deep Space One (DS1) mission. This software was implemented in C and contained some known defects at launch that are detectable with a model checker. We describe the model checking process, the tools used, and the methods and conditions necessary to successfully perform model checking on the DS1 flight software.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Using SPIN model checking for flight software verification


    Contributors:


    Publication date :

    2002-01-01


    Size :

    840634 byte




    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    Using SPIN model checking for flight software verification

    Gluck, P. R. / Holzmann, G. J. | NTRS | 2002


    2.0303 Using Spin Model Checking for Flight Software Verification

    Institute of Electrical and Electronics Engineers | British Library Conference Proceedings | 2002


    Using SPIN model checking for verification of flight software

    Gluck, P. R. / Holzmann, G. J. | NTRS | 2002


    Program Model Checking Using Design-for-Verification: NASA Flight Software Case Study

    Markosian, Lawrence Z. / Mansouri-Samani, Masoud / Mehlitz, Peter C. et al. | IEEE | 2007


    Verification of flight software with Karnough map-based checking

    Jaw, L. / Tsai, W.T. / Homan, D. et al. | Tema Archive | 2007