# Presentation: 329890

## Commercial Displays Model Checking

- Display Management Logic

## Avionics Display Project DCA

**New Commercial aircraft under development**
**DCA – The Displays and Crew Alerting System being developed by Rockwell Collins.**
- Provides primary flight information to the flight crew
**Display Management – Application within the DCA system that is responsible for allocation of display system resources and management of redundancy.**

*(Display system similar to current project)*

## The Problem of Display Management

**Display management requirements state that the DCA system:**
- Must keep the highest priority displays available to the pilots as long as there are sufficient system resources to do so.
- Must keep the Captain’s and First Officer’s Display processes separate as long as there are sufficient system resources to do so.
**Display management can be viewed as a state machine having a very large number of states.**
**Simulink models were used to develop the display management design.**

## The Problem of Display Management

**Due to the flight critical nature of the display management function, it is imperative that the display management function design is complete and correct.**
**The customer requires display system functionality early in aircraft development cycle.**
**In prior development programs this level of maturity was often not achieved until verification testing could be preformed on the target hardware.**
- Problems found during testing late in the development are expensive to correct and cause delays in the development schedule.

## Model Checking Benefits

**Find and correct errors early in the development cycle.**
- Model checking was started prior to the software coding, in parallel to system design.
- Errors are easier and far less expensive to fix at this stage.
**Gain better understanding of the system requirements and uncover missing requirements.**
- Properties are precise statement of system requirements
- Writing properties uncovers ambiguities in English text requirements
**Gain high-level of confidence in correctness of models**
- Expect shorter test cycle and fewer bugs

## DCA Application Architecture

**DCA application consists of 5 main subsystems**
**We are analyzing 4 of the 5 subsystems**
**Remaining subsystem is considered less critical**

| Subsystem | Number of Subsystem Instances | Number of Basic Blocks | Reachable State Space | Number of Properties | Confirmed Errors Found to Date |
| --- | --- | --- | --- | --- | --- |
| 1 (GG) | 1992 | 6125 | 7.87 * 1013 | 43 | 56 |
| 2 (PS) | 131 | 490 | 5.09 * 1021 | 20 | 8 |
| 3 (DUS) | 488 | 1375 | > 1035 | 123 | 5 |
| 4 (CM) | 451 | 2421 | 5.219 * 1027 | 187 | 0* |
| Totals: | 3062 | 10411 | N/A | 373 | 69 |

- * = several open problem reports, but still early in analysis process

## Model Checking Subsystem 1

**Display Resource Redundancy Management – Subsystem 1**
**The model checking process identified 43 formal properties for this model.**
**The initial run of the tools produced 27 counterexamples.  **
- Model checker generates one counterexample per property violated
- Model contained several violations of some properties
- Number of design problems > Number of counterexamples
**After several iterations of development and model checking, all of the errors in the design were located and corrected**
**During the process several counter examples were discovered to be caused by discrepancies in the original English text requirements.**
- Each discrepancy was reviewed with the customer and updates were made as appropriate.
**Subsystem 1 model now completes with no counterexamples (June 2005)**

## Tech Transfer & Process Improvements

- Translation Time: 1-4 HoursTurnaround: 1 Day to 1 Week

- Translation Time: 10 MinutesTurnaround: 3 Hours to 2 Days

- Translation Time: 10 MinutesTurnaround: 10 Minutes

- ATC Group(Beige)

- Dev. Group(Blue)

## Model Checking on the DCA system

**Find errors early in development cycle**
- Model Errors
- Requirements Errors
- Additional Requirements
**Considers corner cases that are difficult to find during test**
**Quick feedback**
- Model checker proves/disproves property in seconds
- Possible to do “tight-loop” development
**Our development group now runs model checker without assistance**
- Tool chain is fairly straightforward
- Writing properties still requires some help
**Useful part of our tool chain**