Model checking is a verification technique developed in the 1980s that has a history of industrial application in hardware verification and verification of communications protocol specifications. Program model checking is a technique for model checking software in which the program itself is the model to be checked. Program model checking has shown potential for detecting software defects that are extremely difficult to detect through traditional testing. The technique has been the subject of research and relatively small-scale applications but faces several barriers to wider deployment. This paper is a report on continuing work applying Java PathFinder (JPF), a program model checker developed at NASA Ames Research Center, to the Shuttle Abort Flight Management system, a situational awareness application originally developed for the Space Shuttle. The paper provides background on the model checking tools that were used and the target application, and then focuses on the application of a "Design for Verification" (D4V) principle and its effect on model checking. The case study helps validate the applicability of program model checking technology to real NASA flight software. A related conclusion is that application of D4V principles can increase the efficiency of model checking in detecting subtle software defects. The paper is oriented toward software engineering technology transfer personnel and software practitioners considering introducing program model checking technology into their organizations.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

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


    Beteiligte:


    Erscheinungsdatum :

    2007-03-01


    Format / Umfang :

    437092 byte





    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    Using SPIN model checking for flight software verification

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


    Using SPIN model checking for flight software verification

    Gluck, P.R. / Holzmann, G.J. | IEEE | 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


    Case Study: NASA Space Shuttle Flight Control Software

    Panel on Statistical Methods in Software Engineering | British Library Conference Proceedings | 1996