# Presentation: 066120

## A Spectrum of IV&V Modeling Techniques 

- Mats Heimdahl (Co-PI)
- Jimin Gao (RA)
- University of Minnesota
- Tim Menzies (Co-PI)
- David Owen (RA)
- West Virginia University/NASA IV&V
- Sanjai Rayadurgam (RA)
- University of Minnesota—Today’s Speaker

## Model-Based Development

- Specification Model

## ROI with Model Based Development

- Source: Esterel Technologies

- - 37.5 %

- - 25 %

- - 75 %

- - 50 %

## Model-Based DevelopmentComing to projects everywhere—soon

- Model based development in some form will in the near future be the norm in critical systems development
- Airbus Industries require the use of model based techniques from all vendors
- Boeing currently evaluating **what** to require—not **if** they will require something
- Honeywell and Rockwell Collins are fielding the capabilities within the next two years
- Etc., etc.

## Model-Based Development Tools

- Commercial Products
- Esterel Studio and SCADE Studio from Esterel Technologies
- Rhapsody from I-Logix
- Rose Real-Time from Rational
- Simulink and Stateflow from Mathworks Inc.

## Model-Based Tools-2

- NASA tools
- STANLEY/LIVINGSTONE for  Integrated (or Intelligent) Vehicle Health Maintenance (IVMS) for second-generation shuttle.

## RSML-e and Nimbus

- RSML*-e* Formal Models (~20 running concurrently)

- Java Simulations of environment

-  Integration in MatLab
-  Test case generation
-  Model checking
-  Theorem proving

- Project with Rockwell Collins Inc.

## Typical Requirements IV&V Process

- Formal Model of SUS

- Initial Assessment Using Low-Cost Approach

- Formal Inspection

- Formal Analysis

- System Under Study
- (typically English)

- Formal Model of SUS

- Inspection

- Inspection

- Inspection

- Automation

- Model
- Extraction

## Model-Based IV&V Process

- Model v.1

- Model
- Evolution

- Model v.2

- Model v.n-1

- Model v.n

- Model
- Evolution

- Model
- Evolution

- Code

- Test

**Increased Effort and Cost**

## Challenges in the New Process

**Scalability and cost of the formal analysis**
**State space explosion problems in model checking**
**Cost effective model evolution**
**Process and guidelines for evolving the model**
**Early and cost effective problem detection**

- Formal Analysis

- Test

- Inspection

- Model v.1

- Model
- Evolution

- Model v.2

- Model v.n-1

- Model v.n

- Formal Analysis

- Test

- Inspection

- Model
- Evolution

- Model
- Evolution

- Code

- Test

## Scalable Analysis

- Model checking is plagued by state space explosion problems
- Are there alternative, possibly heuristic, approaches that are effective?

**Alternate representations**
**NAYO: a no-and-yes-or graph**
**Hypothesis:**
**NAYOs can be used to evaluate models**
**Express interesting properties**
**Find interesting problems**
**NAYO-based evaluation scale**
**NAYO can be used across the model evolution cycle**

**Work with**
**David Owen,**
**WVU**

**Q:** NAYOs can be used to evaluate models?
- 	A: Yes!!  (using a novel stochastic
-                 search engine- ISSRE02)

**Q:** Does NAYO-based evaluation scale?
- 	A1: Stochastic search linear time!
- 	A2: NAYO stochastic search always plateau!
- 	A3: False negative rate falls to zero in the plateau

**Work with**
**David Owen,**
**WVU**

- Some Results

**Notes:**
Each dot is a seeded error..
All errors found.

## Open Issues

- If the stochastic search does not find problems, are there none?
- Compare the stochastic results with full verification on realistic models
- Experiments using:
- RSML*-e*
- Nimbus
- SMV
- Stochastic search
- Flight guidance models from Rockwell Collins

- How to perform model evolution?
- Large case study with Rockwell Collins
- RSML*-e* suitable for the full spectrum of models
- Does finding problem in early models indicate a problem system?
- Does elimination of problems early reduce problems in subsequent models (even if substantially different)?
- Very difficult to assess
- No experiment this year
- Planning for controlled experiment

## Analysis Experiment

**Available Resources:**
- 6 RSML*-e* models of Flight Guidance System from Rockwell Collins Inc.
- Collection of desirable properties
- Translator from RSML*-e* to
- SMV
- FSM suitable for stochastic search
**Experimental Method:**
- Seed errors in the FGS models
- Apply stochastic search as well as full formal verification
- Compare performance and detection capability

- RSML*-e*
- Spec.

- SMV
- Spec.

- NAYO Graph

**Automatic****Translation**

**Automatic****Translation**

**Work with**
**Jimin Gao,**
**U of Minnesota**

## Summary

- Model based development is here
- Or, will be here shortly
- Great potential to improve quality and decrease cost of IV&V
- Must meet some crucial challenges first
- Scalability of formal analysis
- In particular, state space exploration—model checking
- Evolution of models

- Stochastic state space exploration may hold the key
- But, we need to explore
- The fault detection capability of stochastic search
- The efficiency of stochastic search
- Rigorous experiments are starting as I speak
- We will also evaluate alternative analysis tools
- SAL from SRI