# Presentation: 513349

## Model-Based Design & Analysis

**Dr. Steven P. Miller**
**Advanced Computing Systems**
**Rockwell Collins**
**400 Collins Road NE, MS 108-206**
**Cedar Rapids, Iowa 52498**
**spmiller@rockwellcollins.com**

## What Problem are We Solving?

**Safety-Critical Software Is Too Expensive**
**Safety-Critical Software Is Often Wrong**
**DO-178B Certification Is Too Expensive**

***Cut Development Costs/Cycle Time in Half***

***Find 10x More Errors than Current Methods***

***Already Applying This to DO-178B Developments***

## Then and Now

**Model-Based Development Routinely Dismissed**

**Five Years Ago**

**Today**

**Verifying Representative Examples**

**Widespread Acceptance**
***787, FCS 5000, ARJ, MUE, FMS ...***

**Formal Methods Viewed as Impractical & Too Expensive**

**“****This is Buck Rogers!”**
***actual customer quote***

**Created Models by Hand Using Research Notations**

**Automatically Translate Models from Leading Commercial Tools**

**Finding Real Errors in Real Systems **

**Tools were Research Prototypes**

**Tools being Matured for Enterprise Use and Support**

**- in Weeks**

**- in Seconds**

## Outline of Presentation

**	****	****Introduction**
**	****	****Our Approach**
**	****	****Developing the Technology**
**	****	****Making Technology Transfer Happen**
**	****	****Recent Successes**
**	****	****What’s Next?**

## 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, ...

## Rockwell Collins

**Headquartered in Cedar Rapids, Iowa **
**16,000 Employees Worldwide**

## RCI Advanced Technology Center

**RCI Advanced Technology Center**

- The Advanced Technology Center (ATC) identifies, acquires, develops and transitions value-driven technologies to support the continued growth of Rockwell Collins.
- The Automated Analysis group applies mathematical tools and reasoning to the problem of producing high assurance systems.** **

- Commercial Systems

- Government Systems

- Advanced Technology Center

## 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**
**	****	****Our Approach**
**	****	****Developing the Technology**
**	****	****Making Technology Transfer Happen**
**	****	****Recent Successes**
**	****	****What’s Next?**

## Convergence of Two Trends

- Model-Based
- Development

- Automated
- Analysis

*A Revolutionary Change in How *
*We Design and Build Systems*

## Model-Based Development Examples

**Notes:**
Much of our interest in model-based development has been driven by claims of dramatic reductions in cost and improvements in quality by some of our customers and competitors.
For example, large portions of the Airbus A340 and Eurocopter were developed using the SCADE toolset from Esterel. 
What I find exciting about this is that the most successful examples seem to be those in which the modeling language has a precise, formal semantics. 
Even though these are called model-based development, they are really examples of the large-scale industrial use of formal methods.

## Does Model-Based Development Scale?

**Systems Developed Using MBD**
**Flight Control**
**Auto Pilot**
**Fight Warning**
**Cockpit Display**
**Fuel Management**
**Landing Gear**
**Braking**
**Steering**
**Anti-Icing**
**Electrical Load Management**

- Airbus A380

- Length 			239 ft 6 in
- Wingspan 		261 ft 10 in
- Maximum Takeoff Weight 	1,235,000 lbs
- Passengers		Up to 840
- Range			9,383 miles

## How Do We Reduce Costsand Improve Quality?

**Requirements**
**Elicitation**

**Modeling**

**Simulation**

**Automated**
**Analysis**

**Autocode**

**Autotest**

**Reuse**

**Cheaper Than Manual Analysis**

**Finds the Really Hard Errors**

- 10%

- 10%

- 15%

- 5%

- 10% - 20%

**Notes:**
The first phase in model-based development is elicitation. This is where the broad needs of the customer are identified. 
This is usually done through informal techniques such as writing requirements in English, developing use cases, or creating mock-ups.
To demonstrate how this approach can be integrated with existing practices, we took a very simple, traditional approach to elicitation.

## Outline of Presentation

**	****	****Introduction**
**	****	****Our Approach**
**	****	****Developing the Technology**
**	****	****Making Technology Transfer Happen**
**	****	****Recent Successes**
**	****	****What’s Next?**

## Flight Guidance System Mode Logic

**Requirements**
**Elicitation**

**Modeling**

**Simulation**

**Automated**
**Analysis**

**Autocode**

**Autotest**

**Reuse**

**Notes:**
The first phase in model-based development is elicitation. This is where the broad needs of the customer are identified. 
This is usually done through informal techniques such as writing requirements in English, developing use cases, or creating mock-ups.
To demonstrate how this approach can be integrated with existing practices, we took a very simple, traditional approach to elicitation.

## Captured Requirements as Shalls

**Notes:**
We decided to simply capture the requirements as shall statements in a DOORS database, much as is currently done on a large number of projects.

While this probably seems very mundane, later I’ll show you how we changed this into something that I think is very exciting.

## Modeling

**Requirements**
**Elicitation**

**Modeling**

**Simulation**

**Automated**
**Analysis**

**Autocode**

**Autotest**

**Reuse**

**Notes:**
In the next phase, modeling, we start with the informal statement of needs identified during during elicitation, and begin creating a model that defines the desired behavior.
When we started this project back in 1999, we didn’t fee that there was a suitable commercial modeling tool available,  so we decided to use a derivative of the RSML language that was used by Nancy Leveson’s group to specify TCAS, called RSML-e.
RSML-e is a synchronous, data flow language designed for the specification of requirements that includes support for hierarchical finite-state machines. 
We’ve used RSML-e to model the mode logic of a Flight Guidance System and the vertical navigation component of a Flight Management System. Each of these specifications are about 150 pages long. I should also point out that they are representative examples, and don’t describe the behavior of an actual fielded product.

## Modeling Notations

- node Thrust_Required(   FG_Mode : FG_Mode_Type ;    Airborne : bool ;    In_Flare : bool ;    Emergency_Descent : bool;    Windshear_Warning : bool ;      In_Eng_Accel_Zone : bool ;    On_Ground : bool) returns (IsTrue : bool) ;
- let
- IsTrue =    (FG_Thrust_Mode(FG_Mode) and     Airborne)  or
-    (Airborne and Emergency_Descent)  or
-    Windshear_Warning
-  or
-    ((FG_Mode = ThrottleRetard) and      In_Flare)  or
-    (In_Eng_Accel_Zone and On_Ground) ;
- tel ;

**Textual (Lustre, PVS, SAL, ...)**

**Tabular (RSML****-e****, SCR) **

**Graphical (Simulink, SCADE) **

**Notes:**
This shows a fragment of the RSML-e specification for the Flight Guidance system that defines when the Flight Director Guidance cues are to be turned on.
RSML-e was designed to be both readable and mathematically precise. To achieve this, it makes heavy use of tabular specifications that are easily understood by both engineers, pilots, and customers. While this works quite well, its been our observation that most engineers want a graphical, not tabular, specification.
While we’ve been very happy with RSML-e, it appears that the merger of Esterel and SCADE has produced a commercial tool that will meet our needs, and we’re now in the process of converting over to the SCADE toolset on our project.

## Simulation

**Requirements**
**Elicitation**

**Modeling**

**Simulation**

**Automated**
**Analysis**

**Autocode**

**Autotest**

**Reuse**

**Notes:**
While we show simulation is shown as the phase after modeling, simulation and modeling are actually closely intertwined. 
During simulation, we combine our models with an execution engine and mock-ups of the user interfaces. 
This gives the developers a quick and easy way to validate their model of the requirements.

## Simulation

**Notes:**
This slide shows an example of our simulation environment. Here we see the Flight Guidance System mode logic and the Flight Management System Vertical Navigation function executing in the RSML-e simulator. The simulator is displaying a high-level summary of the state machines associated with each model.
We also have a three-dimensional model of the flight-plan and the aircraft, and mock-ups of the Flight Control Panel and the Primary Flight Displays. Time doesn’t allow me to run the simulation right now, but I’d be happy to demonstrate it for you later if you’d like.
We’ve found the simulation of requirements models valuable for at least two reasons. First, we can find many specification errors quickly and relatively cheaply. Second, it makes makes the design accessible to everyone, not just the engineers. This can be invaluable in getting customer feedback early in the life-cycle.
However, simulation suffers from the same problem that testing does, which is “How do you know when you’re done?”  Just as with testing, we can’t expect to find all errors through simulation. 

## Automated Analysis

**Requirements**
**Elicitation**

**Modeling**

**Simulation**

**Automated**
**Analysis**

**Autocode**

**Autotest**

**Reuse**

**Theorem Provers**

**Model Checkers**

**Notes:**
However, since our models have a sound formal semantics, this opens the door for us to apply formal analysis tools such as theorem provers and model checkers to detect many of the errors that simulation would miss.

Unlike simulation, which checks only for inputs we select, analysis offers the benefit of checking our models for all possible combinations of inputs. For this reason, it is much better at looking in the dark corners for those problems that you would only stumble across during simulation.

We are using the NuSMV model checker and the PVS theorem prover from SRI.

## 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!***

## 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.

## Translated Shalls into SMV Properties

**Notes:**
At first, we started by only verifying properties of the mode logic that we considered safety properties, which is to say, those that could put the aircraft in a hazardous state, but we soon realized that all our functional requirements written as shall statements could be specified as properties over our model.
So we went back to our DOORS database and translated each of our shall statement into a CTL property.

## Validate Requirements through Model Checking

**Proved Over 280 Properties in Less Than an Hour**
**Found Several Errors**
**Some Were Errors in the Model**
**Most Were Incorrect Shalls**
**Revised the Shalls to Improve the Requirements**

**Notes:**
We are able to prove all 280 requirements of the mode logic using the NuSMV model checker in about an hour. 
In the course of doing this, we discovered several errors that had been missed during the elicitation, modeling, and simulation phases.  
One entire class of errors were related to what the system should do if more than one input variable should change in the same step. For example, what is the correct behavior if the FMS requests a mode change at the same time that the pilot presses a button on the Flight Control Panel.
This demonstrates how formal analysis complements the more traditional verification activities, and can do it before a single line of code is written.

## What are Theorem Provers?

**Available Since Late 1980’s**
**Widely Used on Security and Safety-Critical Systems**
**Use Rules of Inference to Prove New Properties**
**Also Consider All Combinations of Inputs and States**
**Also Equivalent to Testing with an Infinite Set of Test Cases**
**Generate An Unprovable Proof Obligation if a Property is False**
**Not Limited by State Space**
**Applicable to Almost Any Formal Specification**
**Limitations**
**Require Experience - About Six Months to Become Proficient**
**Constructing Proofs is Labor Intensive**

**Notes:**
Theorem provers are the other class of advanced analysis tools we’ve investigated. Theorem provers have been available since the 1980’s.  They’ve been widely used on security and safety-critical systems.
Like model-checkers, theorem provers consider all possible combinations of inputs and states, and are equivalent to testing with an infinite set of test cases. 
However, instead of conducting a search of the global state space, they use rules of inference to prove new properties about a given specification. As a result, they are not limited by the size of the state space and can be used on almost any formal specification.
Their primary limitation is that they require considerable expertise to use them correctly.  It usually takes about six months to become proficient.  And even for an experienced user, constructing a proof can be quite labor intensive compared to a model-checker.

## Theorem Proving Using PVS

- Model

**Engineer**

**Automated Proof**

**Notes:**
The process for verifying properties using a theorem prover such as PVS looks much the same as for a model checker, but there are some important differences.
Just as with a model checker, we translate the RSML-e model into the PVS language with the translator written for us by the University of Minnesota.  
Just as with NuSMV, we’ve found it is not a problem to state properties directly in PVS, so we’ve deferred the development of property translator.
One of the advantages of theorem proving is that since we won’t be doing a state space exploration, we don’t need to first perform any abstractions on the model.
While we would like the proof process to be fully automated, the price we pay for this is that we still need a human being to guide the theorem prover.

## Searching for Potential Sources of Mode Confusion

**Used Theorem Proving to Search For**
**  ****Entry and Exit of Off Normal Modes**
**  ****Ignored Operator Commands**
**  ****Certain Forms of Lack of Feedback**
**  ****Hidden Modes**
**  ****Unintended Side Effects**
**  ****Lack of Feedback from Multiple Operators**

***Discrepancy between the perceived and***
***actual state of an automated system.***

## Validate Requirements Using Theorem Proving

**Proved Several Hundred Properties Using PVS**
**More Time Consuming that Model-Checking**
**Use When Model-Checking Won’t Work**
**Models that are Numerically Intensive**
**Automated Safety          (Fault Tree) Analysis**

**Notes:**
We have used the PVS theorem prover to prove several hundred properties of the FGS. 
Some of these are quite complex, but most are very simple properties that are used to automated the proofs of the larger properties.
For the mode logic, proving properties using PVS was harder than using a model checker.  
But this is largely because the mode logic consists entirely of Boolean and enumerated types.
In other domains, such as our Vertical Navigation model, that make heavy use of integers and reals, a model checker is much harder to use. 
Those are the problems where a theorem prover can prove valuable.

## Outline of Presentation

**	****	****Introduction**
**	****	****Our Approach**
**	****	****Developing the Technology**
**	****	****Making Technology Transfer Happen**
**	****	****Recent Successes**
**	****	****What’s Next?**

## Original Tool Chain

- RSML-e

- NuSMV Model Checker

- PVS Theorem Prover

- Rockwell Collins/U of Minnesota

- SRI International

**RSML****-e**** to NuSMV**
**Translator**

**RSML****-e**** to PVS**
**Translator**

## Conversion to SCADE

- Esterel Technologies

- Rockwell Collins

- Design
- Verifier

- SRI International

- SCADE

- Lustre

- NuSMV

- PVS

- Safe State
- Machines

## Extension to MATLAB Simulink

- Esterel Technologies

- Rockwell Collins

- Design
- Verifier

- MathWorks

- SRI International

- SCADE

- Lustre

- NuSMV

- PVS

- Safe State
- Machines

## Lustre Translator Framework

**Lustre Translator Framework**

**Small Source-To-Source Transformations**
**Deal with One Language Aspect at a Time**
**Product Family of Small Translators Supports Reuse**

**Lustre Code**

**Target Code**

**Translator**

## Current Tool Chain

- Esterel Technologies

- Rockwell Collins

- Design
- Verifier

- MathWorks

- SRI International

- SCADE

- Lustre

- NuSMV

- PVS

- Safe State
- Machines

- Reactive Systems

## Translator Optimizations for NuSMV

| 
Model | CPU Time
(To Compute Reachable States) |  | 
Improvement |
| --- | --- | --- | --- |
|  | Before | After |  |
| Mode1 | > 2 hours | 11 sec |  |
| Mode2 | > 6 hours | 169 sec |  |
| Mode3 | > 2 hours | 14 sec |  |
| Mode4 | 8 minutes | < 1 sec | 480x |
| Arch | 34 sec | < 1 sec | 34x |
| WBS | 29+ hours | 1 sec | 105,240x |

## Original Tool Chain

- RSML-e

- NuSMV Model Checker

- PVS Theorem Prover

- Rockwell Collins/U of Minnesota

- SRI International

**RSML****-e**** to NuSMV**
**Translator**

**RSML****-e**** to PVS**
**Translator**

## Current Tool Chain

- Esterel Technologies

- Rockwell Collins

- Design
- Verifier

- MathWorks

- SRI International

- SCADE

- Lustre

- NuSMV

- PVS

- Safe State
- Machines

- Reactive Systems

## Outline of Presentation

**	****	****Introduction**
**	****	****Our Approach**
**	****	****Developing the Technology**
**	****	****Making Technology Transfer Happen**
**	****	****Recent Successes**
**	****	****What’s Next?**

## Example 1FCS 5000 Mode Logic

**Example 1****FCS 5000 Mode Logic**

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

**6.8 x 10****21**** Reachable States**

**Mode Controller B**

**Mode Controller A**

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

**Found 24 Errors to Date**

## Example 2 – 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**
**	****	****Our Approach**
**	****	****Developing the Technology**
**	****	****Making Technology Transfer Happen**
**	****	****Recent Successes**
**	****	****What’s Next?**

## Extending the Verification Domain

**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**

** **

## Requirements Based Test Case Generation

**Conformance Testing**
**Autogenerate Test Cases From Model **
**Commercial Tools Available**
**(T-VEC, REACTIS)**
**Show Code *****Conforms***** to the Model**
**Goal is Structural Coverage (MC/DC)**

**Requirements Based Testing**
**State Requirements as Properties**
**Use Bounded Model Checker to Generate Test Cases**
**Goal is to Cover the Requirement**

**Code**

**Model**

**Requirements**

**Properties**

## System Architectural Modeling & Analysis

## Model-Based Safety Analysis

**Add Fault Model for Physical System**

**Model the Digital Controller Architecture**

**Automation Enables “What-If” Consideration of System Designs**

**and Digital Controller Architecture**

**Integrates System and Safety Engineering About a Common Model**

**and the Physical System**

**Notes:**
Steve’s slide 

## Model-Based Safety Analysis

**Common Model for Both System and Safety Engineering**
**Safety Analysis Based on a Formal System Model **
**Facilitates C*****onsistency***** & *****Completeness***** in Safety Analysis**
**Reduced Manual Effort in Error-prone Areas**
**Automated Support for Safety Analysis**
**Explore Various Failure Scenarios**
**Focus on Review on Assumptions in the Models**
**Is the System Model Correct?**
**Is the Fault Model Complete?**
**Assume the (Automated) Analysis is Trustworthy**
**Wide Applicability (Aircraft, UAVs, Shuttle, Space, ...)**

## Verification of Adaptive &Autonomous Systems

## Summary

**Model-Based Development Routinely Dismissed**

**Five Years Ago**

**Today**

**Verifying Representative Examples**

**Widespread Acceptance**
***787, FCS 5000, ARJ, MUE, FMS ...***

**Formal Methods Viewed as Impractical & Too Expensive**

**“****This is Buck Rogers!”**
***actual customer quote***

**Created Models by Hand Using Research Notations**

**Automatically Translate Models from Leading Commercial Tools**

**Finding Real Errors in Real Systems **

**Tools were Research Prototypes**

**Tools being Matured for Enterprise Use and Support**

**- in Weeks**

**- in Seconds**