# Presentation: 099908

## Strategic Investments Research ProgramTechnical Accomplishment

**Shown:**  The application of model checking to the DEOS real-time embedded aerospace operating system from Honeywell to discover a subtle error not uncovered using the testing techniques required for FAA certification. This impact of this error during flight could have been starvation of critical real-time flight calculations. Indicate the scaling of model checking by showing the average factor of increase in lines of code (yellow) and state-space handled (white) by each technique developed and, in the middle, a graph indicating the impact of these techniques with respect to the time taken to analyze a 1000 lines of code.
**Accomplishment / Relation to Milestone and ETG: **Development of the Java PathFinder model checker, with accompanying set of synergistic verification technologies (including, abstractions, slicing, partial-order reduction, intelligent search and environment generation techniques) to enable the efficient analysis of object-oriented, concurrent programs such as those found in the next generation of avionics systems (e.g. the DEOS O/S for Integrated Modular Avionic systems). These model checking technologies have significantly reduced the effort required to analyze avionics software: currently we analyze 1000 lines of code per day compared to state of practice of 50 LOC/day in 1998.
**Future Plans: ** Develop techniques to allow guarantees for correct behavior under certain assumptions that can be checked during actual execution using run-time program monitoring.  Also, development of “learning” algorithms whereby the model checker’s search strategy can be adapted according to the structure of the program being analyzed.

**High-Assurance Software Design**
- POC: Michael Lowry (Ames Research Center)
- February 2002

- ETG: Provide increased confidence and lower the cost of development of next generation avionics software

- Strategic Investments Research ProgramTechnical Accomplishment

## Strategic Investments Research ProgramHigh-Assurance Software Design

- Strategic Investments Research ProgramHigh-Assurance Software Design

**Slicing**

**Abstraction**

**Environment**

**JPF ****Model Checker**

**Repair**

**DEOS****10000 lines to 1500**

**Property ****preserving**

**DEOS**
**Infinite state to 1,000,000 states **

**Semi-automated and requires domain knowledge**

**Heuristic search**
**Focused search for errors **

**Partial-order reduction**

**Spurious error****elimination during****abstraction**

**State compression**

**Bandera code-level debugging of  error-path**

**3x**

**30x**

**5x**

**100x**

**2x**

**15x**

**2x**

**10x**

**2x**

**10x**

**Combined techniques allows **
***O*****(10****2****)**** source line and *****O*****(10****6****)**** state-space increase **
**over state of practice**

**Generation**

**Notes:**
The outer cycle in this slide indicates the analysis path taken when using the JPF model checker. 
A program is sliced with respect to the property being checked. For DEOS there was reduction from 10000 lines to 1500 lines at this step.
The resulting program is then abstracted and an environment is created to represent how the code will be executed (this is like a test-harness used in testing). DEOS required abstraction that reduced the state space from being infinite to being in the order of 1 million states.
 Next the model checker is applied. Each of the core technologies in the model checking phase are given as well.
 If a bug is found the execution path to the error is analyzed on the code-level and the error repaired. The picture shows a screen dump from the Bandera tool that we use to analyze errors.

The yellow and white numbers represent the factor of code size (yellow)  and the size of the state-space (white) increase that each technology on average achieves when applied during analysis. For example, when applying slicing one can expect on average to analyze systems that are 3 times bigger in terms of code size (i.e. lines of code) and 30 times bigger in state-space size than without using slicing.  In the middle-top the accumulative  effect of these synergistic technologies are given as an order of improvement: order 100 in code size and order 1000000 for state-space size.

In the middle of the slide we show the improvement in analysis time and effort given by the technologies we have developed over the duration of the Automated Software Engineering Group’s existence   (from 1997 to 2001). The graph shows the amount of code one person can analyze in a day (in 1000 lines of code) from 1997 when we had no in-house tools, to the present where we have the JPF model checker can the listed synergistic technologies to aid the analysis. The numbers are based on real data: Remote Agent analysis (1997), DEOS analysis (1998-2001) and an autopilot tutor developed at NASA Ames (2001).