• The paper analyses NASAs Java PathFinder (JPF) - a program model checker for the SAFM (Shuttle Abort Flight Management) system.
• The model checking tools used in the paper are limited by the size of the state space. SAFM's size was 'too large' to allow program model checking in its entirety.
• However the application of model checking is modular - which significantly reduces the size limitation.
• The paper states that the D4V approach to designing the program suppresses many limitations of program model checking.
• D4V guidelines:Avoid redundancy, use polymorphism, Leverage model-based design, use finite state machines, use platform-Independent Libraries and Abstraction Layers, reduce concurrency, reduce number of threads, reduce number of interleavings.
• Many D4V issues were identified in SAFM - the main one being complexity.
• Markosian introduces a subtle bug into the program and two approaches to detecting the bug (traditional inspection and model checking) were implemented.
• The D4V guideline violation by SAFM involves a complex conditional-statement in order to decide the type of scenario to run next - a violation similar to the reduced use of polymorphism.
• The paper states that the model checker checks only one choice of scenario, and not the entire state space. In order to allow the model checker to detect the bug it must check all branches of the program tree. A D4V approach was implemented in the program which allows the model checker to confirm the bug.
• Statistical analysis of D4V impelmentation in the paper shows a 64% reduction in total bytecode instructions executed, a 25% reduction in the time taken to confirm the bug and a 13% reduction in total memory used.

-- PremNirmal - 2011-07-15