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.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

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




    Publication date :

    2007-03-01


    Size :

    437092 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. | IEEE | 2002


    Using SPIN model checking for flight software verification

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


    Using SPIN model checking for verification of flight software

    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


    Verification of Flight Software with Karnough Map-based Checking

    Jaw, Link / Tsai, W. T. / Homan, David et al. | IEEE | 2007