# Presentation: 513348

## Formal Verification of Flight Critical Software

**Dr. Steven P. Miller**
**Advanced Computing Systems**
**Elise A. Anderson**
**Commercial Systems Flight Control**
**Rockwell Collins**
**400 Collins Road NE, MS 108-206**
**Cedar Rapids, Iowa 52498**
**{spmiller,eaanders}@rockwellcollins.com**

## Concept Overview

- FCS 50000 Flight Control System

## Outline of Presentation

**	****	**
**	****	****Introduction**
**	****	****Model Checking**
**	****	****Specification of the FCS 5000 Mode Logic**
**	****	****Verification of the FCS 5000 Mode Logic**
**	****	****Concluding Remarks**

## Who Are We?

**A World Leader In Aviation Electronics And Airborne/ Mobile Communications Systems For Commercial And Military Applications**

**Notes:**
Some of the systems we build include communications, navigation, flight control, displays, in-flight entertainment, and information management system. 
Perhaps of more interest here, ...

## Automated Analysis Section

**Automated Analysis Section**

**AAMP5 Microcode Verification (PVS)**

**AAMP-FV Microcode Verification (PVS)**

**JEM Java Virtual Machine (PVS)**

**FCP 2002 Microcode (ACL2)**

**AAMP7 Separation Kernel (ACL2)**

**FGS Mode Confusion Study (PVS)**

**FGS Safety **
**Analysis **
**(RSML****-e****)**

**FGS Mode **
**Confusion **
**(RSML****-e****)**

** ****Displays **
**Verification (NuSMV)**

**FCS 5000 FGS **
**Verification (NuSMV)**

**SHADE**
**(ACL2)**

**GreenHills**
**Integrity RTOS **
**(ACL2)**

**1994**

**1996**

**1998**

**2000**

**2002**

**2004**

**2006**

**AAMP5 Partitioning (PVS)**

**NASA **

**NSA**

**1992**

**vFaat**
** ****(ACL2, **
**PVS)**

**AFRL**

**Tech Transfer**

**NASA LaRC Funded**

**NSA Funded**

**AFRL Funded**

**AvSSP**

## Methods and Tools for Flight Critical Systems Project

**Five Year Project Started in 2001**
**Part of NASA’s Aviation Safety Program         (Contract NCC-01001)**
**Funded by the NASA Langley Research Center and Rockwell Collins**
_**Practical**_** Application of Formal Methods To      Modern Avionics Systems**

**Notes:**
This project is a five year effort that started in 2001. It is part of NASA’s Aviation Safety Program, and is funded by the NASA Langley Research Center and Rockwell Collins
The project has a very heavy emphasis on requirements modeling and validation, because that is where we feel we can gain the greatest benefit.
Dr. Mats Heimdahl of the University of Minnesota leads a team that provides tool support for the project. 
To demonstrate that these tools scale to real world problems, engineers at Collins are concentrating on applying these tools to two problem domains, Flight Guidance and Flight Management.
To ensure the long term transfer of these techniques and tools to industry, we have started working with commercial tool vendors, particularly Esterel technologies. 

## Outline of Presentation

**	****	**
**	****	****Introduction**
**	****	****Model Checking**
**	****	****Specification of the FCS 5000 Mode Logic**
**	****	****Verification of the FCS 5000 Mode Logic**
**	****	****Concluding Remarks**

## What Are Model Checkers?

**Breakthrough Technology of the 1990’s**
**Widely Used in Hardware Verification (Intel, Motorola, IBM, ...)**
**Several Different Types of Model Checkers**
**Explicit, Symbolic, Bounded, Infinite Bounded, ...**
**Exhaustive Search of the Global State Space **
**Consider All Combinations of Inputs and States**
**Equivalent to Exhaustive Testing of the Model**
**Produces a Counter Example if a Property is Not True**
**Easy to Use**
**“****Push Button” Formal Methods**
**Very Little Human Effort Unless You’re at the Tool’s Limits**
**Limitations**
**State Space Explosion (10****100**** – 10****300**** States)**

## Advantage of Model Checking

***Testing Checks Only the Values We Select***

***Even Small Systems Have Trillions (of Trillions) of Possible Tests!***

## Advantage of Model Checking

**Advantage of Model Checking**

***Model Checker Tries Every Possible Input and State!***

## Translation Framework

## Example - ADGS-2100 Adaptive Display & Guidance System

**Requirement**
**Drive the Maximum Number of Display Units Given the Available Graphics Processors **

**Counterexample Found in 5 Seconds!**

**Checking 373 Properties**
**Found Over 60 Errors**

**883 Subsystems**
**9,772 Simulink Blocks**
**2.9 x 10****52**** Reachable States**

## Outline of Presentation

**	****	**
**	****	****Introduction**
**	****	****Model Checking**
**	****	****Specification of the FCS 5000 Mode Logic**
**	****	****Verification of the FCS 5000 Mode Logic**
**	****	****Concluding Remarks**

## Flight Guidance System Overview

## Simple Mode Transition Diagram

## Synchronous Composition of Two Mode Transition Diagrams

- 1-z

- 1-z

## Outline of Presentation

**	****	**
**	****	****Introduction**
**	****	****Model Checking**
**	****	****Specification of the FCS 5000 Mode Logic**
**	****	****Verification of the FCS 5000 Mode Logic**
**	****	****Concluding Remarks**

## Summary of Errors Found

**Model-Checking Detected the Majority of Errors**
**Model-Checking Detected the Most Serious Errors**
**Found **_***Early in the Lifecycle ***_**during Requirements Analysis**

| Dectected By | Likelihood of Being Found by Traditional Methods |  |  |  |  |
| --- | --- | --- | --- | --- | --- |
|  | Trivial | Likely | Possible | Unlikely | Total |
| Inspection |  |  | 1 | 2 | 3 |
| Modeling |  | 5 | 1 |  | 6 |
| Simulation |  |  |  |  |  |
| Model Checking | 2 | 1 | 13 | 1 | 17 |
|  Total | 2 | 6 | 15 | 3 | 26 |

## Verification of Individual  Mode Transition Diagrams

**AX AG( LGA ******** AX( Event9 ******** ROLL )) **

**AX AG( LGA ******** AX( (Event4 & !Event6 & !Event9) ******** HDG))**

**AX AG( Event8 ******** LGA ) **

**** False

## Errors Found Verifying Individual Mode Machines

**Model-Checking Found Half the Errors**
**Tended to Find the Less Serious Errors**
**Counter Example Pinpoints Source of the Error**

| Dectected By | Likelihood of Being Found by Traditional Methods |  |  |  |  |
| --- | --- | --- | --- | --- | --- |
|  | Trivial | Likely | Possible | Unlikely | Total |
| Inspection |  |  | 1 | 2 | 3 |
| Modeling |  | 5 | 1 |  | 6 |
| Simulation |  |  |  |  |  |
| Model Checking | 2 | 1 | 6 |  | 9 |
|  Total | 2 | 6 | 8 | 2 | 18 |

## Verification of Composite Machines

**Verification of Composite Machines**

**Requirement**
**Mode A1 => Mode B1**

**5.1 x 10****27**** Reachable States**

**Mode Controller B**

**Mode Controller A**

**Counterexample Found in**
**Less than Two Minutes!**

**Found 8 More Errors**

## Errors Found by Model-Checking Composite Mode Transition Diagrams 

**Errors Found Tended to Be More Serious Errors**
**Checking Relationships Between Mode Transition Diagrams**
**Difficult to Find by Inspections & Simulation**

| Dectected By | Likelihood of Being Found by Traditional Methods |  |  |  |  |
| --- | --- | --- | --- | --- | --- |
|  | Trivial | Likely | Possible | Unlikely | Total |
| Inspection |  |  |  |  |  |
| Modeling |  |  |  |  |  |
| Simulation |  |  |  |  |  |
| Model Checking |  |  | 7 | 1 | 8 |
|  Total |  |  | 7 | 1 | 8 |

## Outline of Presentation

**	****	**
**	****	****Introduction**
**	****	****Model Checking**
**	****	****Specification of the FCS 5000 Mode Logic**
**	****	****Verification of the FCS 5000 Mode Logic**
**	****	****Concluding Remarks**

## Conclusions

**Model-Based Development *****is***** the Industrial Use Formal Specification**
**Convergence of Model-Based Development and Formal Verification**
**Engineers are Producing Specifications that Can be Analyzed**
**Formal Verification Tools are Getting More Powerful**
**Model Checking is Very Cost Effective**
**Simple and Easy to Use**
**Finds All Exceptions to a Property**
**Used to Find Errors Early in the Lifecycle**
**Applied to Models with Only Boolean and Enumerated Types**

**Notes:**
In conclusion, there are just a few observations I’d like to make.
First, model-based development is just another name for the industrial use of formal methods, providing the modeling language has a well-defined semantics.
Second, as John Rushby has pointed out, there is an important convergence occurring in that as engineers start using model-based development, it will enable the use of formal verification.
We will still need several approaches to formal verification. We’ve found model-checking is wonderful when it can be used, but we still need approaches such as theorem proving when it fails.
Constructive requirements models are useful since they be executed, are consistent, and complete, and can be used to autogenerate code and test cases. 
Shalls are just informal property based specifications, and may still be a good way to elicit an informal statement of the requirements. 
Perhaps most interesting, proving the shalls seems to be a very good way of further validating a constructive model.

## Future Directions

**Numerically Intensive Systems**
**Infinite Bounded Model Checkers**
**Decision Procedures for Integers        and Real Numbers**
**Non-linear Arithmetic**
**Automatic Extraction of         Conservative Abstractions**
**Applications**
**Spacing & Trajectory**
**Required Navigation Performance (RNP)**
**Collision Avoidance**
**Advanced Flight Control**

** **

## For More Information

**Alan C. Tribble, Steven P. Miller, and David L. Lempia, *****Software Safety Analysis of a Flight Guidance System*****, NASA Contractor Report CR-2004-213004, March 2004, available at http://techreports.larc.nasa.gov/ltrs/dublincore/2004/cr/NASA-2004-cr213004.html.**
**Alan C. Tribble and Steven P. Miller, Safety Analysis of Software Intensive Systems, IEEE Aerospace and Electronic Systems, Vol. 19, No. 10, pp. 21 - 26, October 2004.**
**Steven P. Miller, Mats P.E. Heimdahl, and Alan C. Tribble, *****Proving the Shalls*****, in Proceedings of  FM 2003: the 12th International FME Symposium, Pisa, Italy, Sept. 8-14, 2003. **
**Alan C. Tribble, David D. Lempia, and Steven P. Miller, *****Software Safety Analysis of a Flight Guidance System*****, in Proceedings of the 21st Digital Avionics Systems Conference (DASC'02), Irvine, California, Oct. 27-31, 2002. **

## Backup Slides

## Model Checking Process

- Model

**Engineer**

**Automated Check**

**Yes!                    **

- SMV
- Spec.

**Automatic Translation**

**Notes:**
The ideal process for checking properties using NuSMV would be to first write both the model and the  properties  in RSML-e, then translate the properties and the model into NuSMV.  
The University of Minnesota has written a translator from RSML-e to NuSMV for us.
The automated verification we get naturally by using the NuSMV model checker.
We have not developed a translator for the properties simply because it has been so straightforward to just write the properties in NuSMV, but this could be added at any time.
Of course, for specifications that involve integers or real numbers, some sort of abstraction may be needed to keep the state space to a reasonable size. The University of Minnesota is currently working automating this process.