# Presentation: 012155

## Component Based Approach for Model Checking

**John D. Powell**
**California Institute of Technology, **
**Jet Propulsion Laboratory**

## Acknowledgments 

**This research was carried out at the Jet Propulsion Laboratory, California Institute of Technology, under a contract with the National Aeronautics and Space Administration.**
** **
**The work was sponsored by the NASA Office of Safety and Mission Assurance under the Software Assurance Research Program lead at the NASA Software IV&V Facility. **
**This activity is managed locally at JPL through the Assurance and Technology Program Office.**** **

## The Flexible Modeling Framework (FMF) & Approach

**Collection of Model Components **

**Model Checker**
** **

**Component Combiner **

- Each Individual Component

- Unique Component Combinations

**If Combination State Space is too Large**

- No

- Yes

**MCCT**

**Implicit**

**Explicit**

**Heuristic Propagation of Results **

- Updated Component 

- Combinations Containing 

## Model Checking  (MC)

- FMF uses MC as its core technology
- Exhaustive search
- Verification of temporal logic properties
- MC limited by an exponential state space explosion
-  *	****m******n****** s.t.****** ******m=val_range, n=|vars|***
***	******Can MC still be useful when the system is large?***

## The Flexible Modeling Framework (FMF) – Part 1

**Collection of Model Components **

**Model Checker **

**Component Combiner **

- Each Individual Component

- Unique Component Combinations

**If Combination State Space is too Large**

- No

- Yes

## FMF Components and Combinations

- FMF models the system (S) as a series of small model components (c***i**** *| 1  *i*  n) which are model checked
- 	**({c****1****, c****2****, c****3****, ... c*****n*****} = S) /\ (c****i**** ******** S)**
- FMF model checks component combinations
- 	(C**k** | (C**k**  S) /\ (1  |C**k**|  m) where the state space of C**m+1** is beyond memory thresholds
***	******What can be done when state space explosion thresholds are reached?***

## The Flexible Modeling Framework (FMF) – Part 2

**Collection of Model Components **

**Model Checker **

**Component Combiner **

- Each Individual Component

- Unique Component Combinations

**If Combination State Space is too Large**

- No

- Yes

**MCCT**

**Implicit**

**Explicit**

**Heuristic Propagation of Results **

## Model Component Combination Tree (MCCT)

- MCCT level *l* = {Ck | (| Ck| = n-*l *)* */\* *(*n* = |S|)}
- MCCT root node (level 0) – full system of n components
- MCCT leaf nodes (level n-(n-1)) – single components
- State space explosion threshold separates the explicit and implicit portions of the MCCT
- Explicit portion – **<C****k****, VV = 2||0, CR = 1>**
- known property verification knowledge from MC results
- Implicit portion – **<C****k****, VV = (2,0), CR = (0,1)>**
- derived verification knowledge from explicit portion of MCCT

## Example: Heuristic VV and CR Propagation

**CR = 1**

- Explicit MCCT

- Implicit MCCT

**0 < CR < 1**

**CR****i**** = 1 – *****p *********

**CR****i+1**** = CR****i**** – *****p *********

**CR = 1 ********

**CR = 1 ********

## Heuristic Propagation

- Verification Values (VV) – degree to which a property holds or does not hold (0 – 2)
- Confidence Rating (CR) – degree of certainty that the VV is correct (0 – 1)
- Why 2 heuristic values instead of 1?
- VV=1, CR=.99 – Confident inconclusiveness
- Known information is highly contradictory
- Variable model component resolution is unlikely to help
- VV=1, CR=.01 – Inconclusive due to heuristics
- Heuristic propagation’s prediction accuracy is degrading
- Variable model component resolution is more likely to help

## Example: Heuristic VV and CR Propagation

**CR = 1**

- Explicit MCCT

- Implicit MCCT

**0 < CR < 1**

**CR****i**** = 1 – *****p *********

**CR****i+1**** = CR****i**** – *****p *********

**CR = 1 ********

**CR = 1 ********

## Variable Component Resolution

- Trading less abstract model components for more abstract ones.
- Increased ability to analyze interaction of more model component
- Decreased detail about the behavior of some model components
- Used to Cope with State Space Explosion
- 	***Model Component resolution versions occur as a side effect of model updates?***

## Future Work

- Validation of Approach and Case Studies
- Multi-Mission Encrypted Communication System
- IP Phone Project
- Collaboration towards alternate propagation methods
- Dr. Tim Menzies & Grad. Students at (West Virginia University / NASA IV&V)
- ??? – Maybe You - ???
- Extend to beyond software/network security

## Conclusion

- Modeling in FMF components is  more compatible with the software development process
- MC of FMF components and combinations allows partial answers to otherwise intractable system state spaces
- The approach could accommodate other MCs with adaptation
- Heuristic propagation provides a means for reasoning about the larger (intractable) system state space through the use of confidence ratings and verification values
- The explicit portion of MCCT is an”oracle” of verification knowledge that may be used with various inference/heuristic/AI methods etc...

## Backup Slides 

## Rapid Model Updating

- FMF benefits software early in its lifecycle
- Earlier Discovery of Software Errors
- Correction is easier / better / less expensive
- FMF must adapt to early lifecycle events
- Rapidly changing requirements and designs
- Varying / Increasing levels of detail defined for different parts of the system.
***How can traditional model development for MC be enhanced to cope with volatile systems?***

## The Flexible Modeling Framework (FMF) – Part 3

**Collection of Model Components **

**Model Checker **

**Component Combiner **

- Each Individual Component

- Unique Component Combinations

**If Combination State Space is too Large**

- No

- Yes

**MCCT**

**Implicit**

**Explicit**

**Heuristic Propagation of Results **

**Updated Component ******

**Combinations Containing ******