# Presentation: 266193

## Model-Validation in Model-Based Development

**Kurt Woodham **
- L-3 Communications

**Ajitha Rajan, Mats Heimdahl **
- University of Minnesota

- OSMA SAS ’08	September 8-12

## Problem: Model Validation

- Model-Based Development (MBD) is here to stay
- Use of MBD is accelerating
- Estimate 50% of NASA development projects using some form of MBD
- Many advantages: model-checking, code generation, desktop testing, closed-loop simulation
- Enhances early detection of requirement, design, or implementation defects
- “Executable Specifications” enable evaluation of behavior that might otherwise be relegated to Inspections and Testing
- How do we know the models are “right”?
- _Manually develop black-box tests_
- When have we validated enough?
- _Measure test coverage on an implementation/model_

## Problem : Current Practice

- Measure black-box test coverage over the model
- Indirect measure
- Defects of omission in model not exposed.
- Executable artifact is necessary
- Adequacy can only be determined late in the development process

- Incomplete Model

**Weak**** **
**Black-Box **
**Test set**

## Goals of Project  

- Goals of Project

***Define metrics for objective, implementation-independent*** measure of adequacy of a black-box test suite
***Develop tools to measure validation adequacy ***based on the defined metrics
- Provide capability for ***autogeneration*** of black-box test suites

## Testing – What does it mean?

- Assertion Based Testing (ABT) to Validate Model

**Our contribution is in providing novel ABT capabilities**

- In General

## What are Assertions?

- Assertions

- Properties/ Formal Assertions

- Defined over

**System**

- in1

- ink

- out1

- outm

- Can also be over components, interfaces,...

## Contributions - ABT

- Assertions

- Black-Box Tests

- Measure Adequacy

- Auto-generate

**2**

**1**

- We provide the following contributions in the Assertion-Based testing domain (indicated by      in the above figure):
***Objective, implementation-independent*** measure of adequacy of a black-box test suite
***Auto-generation*** of black-box validation tests directly from assertions
***Objective assessment*** of completeness of model as well as assertions

## The Idea

*...**then define structural coverage metrics to directly and objectively describe coverage of ****assertions***

*Write ****assertions**** in a formal notation...*

**Synchronous Observers**

**Notes:**
We propose the following idea for an adequacy measure:
Since reqs are declarative statements of what a system should do
You first write reqs in a formal notation....such as temporal logics, which are very similar in structure to the informal declarative statements... or as synchronous observers or state machines, these notations have been used to formally express models, they can also be used to express requirements. 
We then define structural coverage metrics to directly and...These structural coverage metrics provide an objective and impl-indep means of measuring adequacy of black-box test suites. 
Reqs have been formlaized in previous efforts for verfication purposes...tell about the fgs system

## LTL Temporal Operators

**A**

| Operator | Notation | Meaning  |
| --- | --- | --- |
| Globally A | G(A) | Formula A is true in all states |
| Future A | F(A) | Formula A is true in some future state |
| A until B
 | A U B
 | Formula A is true in every state until B becomes true.  B must eventually become true for the property to be true.  |
| Next A | X(A) | Formula A is true in the next state |

- S0

- S1

- S2

- S3

- Si

**A**

**A**

**A**

**B**

**A**

## Formalizing Assertions

*“**If the onside FD cues are off, the onside FD cues shall be displayed when the AP is engaged”*
*G((¬ Onside_FD_On  ****  ¬ Is_AP_Engaged) → X(Is_AP_Engaged → Onside_FD_On))*
- Possible Coverage Metrics
- Assertion coverage: single test case that demonstrates that assertion is satisfied
- Prone to “dumb” tests, e.g., execution in which AP is never engaged.
- More rigorous metric is necessary

**Notes:**
We think LTL is a feasible way of representing formal requirements. 
Requirements are defined informally, as for example, “shall” statements or use cases. However, requirements have been formalized in previous efforts for verification purposes....natural language reqs can be formalized using notations such as temporal logics, and synchronous observers. 
The FGS has 293 informal requirements expressed as shall statements. Consider a sample requirement from the FGS defining how the Flight Director is turned on by the AutoPilot. The engineers at rockwell collins found that it is straight forward to translate these informal shall statements into linear temporal logic properties, and these props were very similar in structure to the natural language requirement. For the sample req here, the ltl prop states that it is globally true that if the onside fd is not on and the AP is not engaged, in the next instance in time if the AP is engaged, then the onside FD will be on. The full set of informal reqs. for the FGS were translated into 293 LTL properties by the production engineers at rockwell collins.
What we propose to do is to define structure coverage metrics over formalized requirements (like the ltl prop shown here), and use these coverage metrics as an adequacy measure for black-box test suites. Thus our proposed measure is implementation-independent. 
What coverage metric would you define over the formal req?  Consider decision coverage over requirements, for a test suite to satisfy this metric, you would need a single....typically this coverage is too weak, since you can derive a lot of useless test cases. For our sample req, to satisfy decision cov, we can create a test case that leaves the  AP disengaged throughout the test....although this test technically satisfies the property, it does not shed much light on the correctness of our model. 
Too weak – also because you only have a single test case for every req....that single test case can be really useless

As mentioned before, we define cov metrics on the structure of formal reqs. In the critical sys domain, there is a close relationship between the high level reqs and the formalized properties. The FGS has 293 informal reqs that were formalized as LTL props in a straight forward manner in a prev effort by Steven Miller and others, and the props were very similar in struc to the natural language req. This slide shows one such natural language req and the corresponding ltl prop. 

## Task - 1

- Define a collection of assertion coverage criteria
- Formalize the assertion coverage obligations

**Notes:**
That’s my first proposed task – to come up with a bunch of rigorous reqs coverage metrics and formalize their obligations .
I will now explain one such reqs cov metric that we defined and formalized in our prelim study. 

## Antecedent Coverage

- Many of the assertions in the FGS are of the form :
*Globally if ‘A’ occurs then ‘B’ will occur*
- 	G (A → B)
- Two ways of satisfying (A → B)
- A is false
- A is true and B is true
- Antecedent Coverage – test cases will exercise the antecedent.

- S0

- S1

- Sn

- Not A

- Not A

- A, B

- What if: ACD → B

**Notes:**
Many of the reqs in the fgs....
When we did reqs cov, that is a test case to illustrate one way in which the req is met...for reqs of the above form, the model checker came back with trivial test cases that go from the initial state to a state where a is false. Such test cases exercise a very small portion of the model and are not very interesting. We knew the reqs cov metric was very weak, but we didn’t really do anything about it. When we sent our paper fro submission, with just the reqs cov and ufc cov...our reviewers also noted that the reqs cov metric is too weak, so it wouldn’t be a fair comparison to the ufc metric. They suggested that we define a better metric so that antecedents in properties like these were exercised. So we ended up defining a new metric – reqs ant. Cov for the final version of our paper and that’s the story behind it
Reqs antecedent cov is a stronger metric, cos it specifies how the req should be satisfied by the test case. For reqs of the above form, the reqs ant cov would require the test case to make the antecedent true at some point in the test path. The test case gen were longer than reqs cov. 
Reqs coverage – trivial test cases that go from initial state to a state where A is false. 
Reqs Ant Cov  A will be true at least once along the satisfying path.

## Modified Condition/Decision Coverage (MC/DC)

- To satisfy MC/DC
- Every point of entry and exit in the model should be invoked at least once,
- Every basic condition in a decision in the model should take on all possible outcomes at least once, and
- Each basic condition should be shown to independently affect the decision’s outcome

| A | B | A or B |
| --- | --- | --- |
| F | F | F |
| T | F | T |
| F | T | T |

- Independent effect of A

- Independent effect of B

- Basic Conditions

**Notes:**
To define a suitable coverage metric over requirements, we decided to adapt a rigorous metric like the MC/DC defined over source code and modeling languages. MC/DC metric is used in the avionics industry for software verification purposes. Or say – software used in the avionics industry is required to be covered upto mc/dc standard or something like that, Before we define our proposed metric, I will give 
A quick run thru of what the mc/dc criteria means. For a test suite to satisfy mc/dc, every point of .....
Every basic cond shld take on all....eg shows a decision ‘A and B’ with atomic conds ‘A’, and ‘B’. The test cases in your test suite shld make sure A takes on both true and false values and so does b. The third point states that each .... Which in our example means, to show indep of A , varying the value of A while holding B at a constant value such that A is not masked out shld change the value of the decision’s outcome. So when you hold b to true, changing A from T to F, will change the outcome from T to F. That’s indep of A, similarly for B
The MC/DC metric defines what “states” in the system satisfies the coverage obligations. 

## Unique First Cause (UFC) Coverage

- “System shall eventually generate an *Ack (A)* or a *Time Out (B)**”*
-  Req. LTL property -  F(A  B) .

**Formal UFC obligation for A :  ****¬****(A ******** B) U (A ******** ****¬****B)**
**	****	****                 ****for B :  ****¬****(A ******** B) U (B ******** ****¬****A)**

- S0

- S1

- S2

- S3

- Si

**A, ¬ B**

**¬A, ¬B**

**¬A, B**

**¬A, ¬B**

**¬A, ¬B**

- Path satisfies UFC obligation for A but not B.

- S0

- S1

- Si

- To show independence of B,

**¬A, B**

**¬A, ¬B**

**¬A, ¬B**

**Notes:**
Consider an informal req ....formalized as...LTL properties define execution ‘paths’, so to define satisfying test paths we need to extend the constraints for  the MC/DC metric to include temporal operators that define constraints over the execution paths. We propose the metric called unique first cause civerage adapted from the MC/DC metric. 
In our metric, UFC, we define independence of atomic condition in terms of the SHORTEST satisfying path for the formulas....rather the first evidence that the formula is satisfied is because of the atomic condition. 
If we have a Formula R and a path π, an atom α in R is the unique first cause if,  in the first state along π in which R is satisfied, it is satisfied because of atom α.
Say that to show independence of B, u would need a path in which the first time the formula is satisfied, it is because of B.
How would express this specific way of staisfying ufc obligations over atomic conditions...we used the ltl notation to express this. Using ltl you can specify how the paths satisfying ufc obligations would look like. Since we have an obligation for every atomic condition in the property, you would end up with 100s of obligations expressed as ltl props for a system like the fgs. These ltl properties now represent the obligations that the black-box test suite would need to satisfy. The black-box test suite should have atleast one test case for every test obligation expressed as an ltl property. 
The UFC obligation to show independence of atomic condition A in this ltl property would be ....and for B it would be..
Paper gives the formalization of UFC coverage obligations over reqs expressed as ltl props. 
Bring up the difference between unique cause coverage here???

## UFC Coverage

**G(*****A*****)*****+**** = *{*A *U* *(*a ***** G(*A*))* | a *є*  A**+*} **G(*****A*****)*****-**** = *{*A* U *a | a *є* A**-*}
**F(*****A*****)*****+**** = *{**¬***A* U *a | a *є* A**+*} **F(*****A*****)*****-****** ****= *{**¬***A *U* (a ***** G(**¬***A*))*| a *є* A**-*}
**(*****A *****U***** B*****)*****+**** = **	*{(*A ***** **¬***B*) U ((*a ******* ¬***B*) ****** **(*A *U *B*)) | *a є A**+*}* **** ******	***{(*A ******* ¬***B*) U *b | b *є* B**+*}
**	****(*****A *****U *****B*****)*****-***** **= 	{(*A ******* ¬***B*) U (*a ******* ¬***B*) | *a *є* A**-*}  	{(*A* ****** ¬***B*) U*** ***(*b ******* ¬**(*A* U *B*)) | *b *є* B**-*}
**X(*****A*****)*****+**** *= {X(*a*) |* a *є* A**+*}**X(*****A*****)*****-****** ****= *{ X(*a*) | *a *є* A**-*}

- Michael Whalen, Ajitha Rajan, Mats Heimdahl and Steven Miller. **Coverage Metrics for Requirements-Based Testing.** In *Proceedings of ISSTA 2006. *

**Notes:**
We define ufc obligations over all the ltl operators, please refer to the paper for more technical information. 
The obligations that we have that a black-box test suite needs to satisfy are as ltl formulas which represent infinite paths...but the test cases we want to measure over represent finite paths...

## Task 2 – Validation Adequacy               Measurement Tool

- Task 2 – Validation Adequacy               Measurement Tool

- We currently support the following coverage metrics:
-  Assertion Coverage
-  Assertion Antecedent Coverage
-  Assertion UFC Coverage

## Task - 3

- Automatically generate requirements-based tests from ...
- Formal assertions
- Abstract model called **Assertion Model **created using assertions and environmental constraints (specified as invariants)
-    ... to provide the defined assertion coverage.

## Automatically Generating Requirements-Based Tests

- Common with the Adequacy Measurement Tool

- Assertions and environmental constraints specified as invariants

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

## Preliminary Evaluation

- Interested in determining:
- Feasibility of generating assertion-based tests from a set of assertions
- Generated assertion-based tests to provide UFC coverage over the assertions
- Effectiveness of these test sets in validating the system model
- Measured MC/DC achieved by the test sets over the system model
- Used three realistic sized examples:
- Flight Guidance System (FGS),
- and two models related to the Display Window Manager system (DWM1 and DWM2)

## Results

- Ajitha Rajan, Michael Whalen, and Mats Heimdahl. **Model Validation using Automatically Generated Requirements-Based Tests.** In *Proceedings of 10th IEEE High Assurance Systems Engineering Symposium, *Nov 2007*. *

## Results and Analysis

- UFC test suites achieved high MC/DC coverage over DWM models – well defined set of assertions
- Test-suite generated for UFC achieved very low MC/DC over the FGS model
- “*When the FGS is in independent mode, it shall be active”.*
*G(m_Independent_Mode_Condition.result → X(Is_This_Side_Active = 1))*

- RSML–e Macro

- Structure of *Independent_Mode_Condition is not captured in the property*

*Independent_Mode_Condition** = ((Is_LAPPR_Active & Is_VAPPR_Active **	**& IS_Offside_LAPPR_Active & Is_Offside_VAPPR_Active) |                       **	**( Is_VGA_Active & Is_Offside_VGA_Active))*

## Benefits of ABT

- Saves time and effort in generating validation test suites from assertions
- Effective method for generating model validation tests when the assertions are well defined
- Helps in identifying missing assertions and over constrained models

## Bonus Task – Adequacy of Conformance Testing

- Bonus Task – Adequacy of Conformance Testing

- Run

- Measure Adequacy

- Measure Adequacy

- Direct assessment of how well tests exercise the assertions
- Will expose defects of omission
- Assertion coverage could necessitate longer test cases than for model coverage

## Assertion Coverage as an Adequacy Measure for Conformance Testing

- Assertion Coverage as an Adequacy Measure for Conformance Testing

**Hypothesis 1(H****1****):** Conformance tests providing assertion UFC coverage are more effective than conformance tests providing MC/DC over the model

**Hypothesis 2(H****2****):** Conformance tests providing assertion UFC coverage *in addition* to MC/DC over the model are more effective than conformance tests providing only MC/DC over the model

## Experiment

- Used four industrial systems :
- Two models from the display window manager
- Two models representing the mode logic of a flight guidance system
- Assessed effectiveness of test suites in terms of their fault finding ability

- Ajitha Rajan, Michael Whalen, Matt Staats, and Mats Heimdahl. **Requirements Coverage as an Adequacy Measure for Conformance Testing.** To Appear in *Proceedings of 10th International Conference on Formal Engineering Methods, *Oct 2008*. *

## Results – Hypothesis 1

- Hypothesis 1 **rejected **at 5% statistical significance on all but the Latctl system

## Analysis – Hypothesis 1

- Model coverage better than assertion coverage for measuring adequacy of conformance test suites
- Assertion UFC coverage is heavily dependent on the nature and completeness of the assertions
- Rigor and robustness of assertion coverage metric used is important
- UFC metric gets cheated when assertions are structured to hide the complexity of conditions

## Results – Hypothesis 2

- Hypothesis 2 **accepted **at 5% statistical significance on all but the DWM2 system

## Analysis – Hypothesis 2

|  | UFC Achieved by MC/DC suites | Achievable UFC | Rel. Diff |
| --- | --- | --- | --- |
| DWM1 | 28.3% | 96.9% | 70.8% |
| DWM2 | 59.7% | 64% | 6.7% |
| Latctl | 94.7% | 99.5% | 4.8% |
| Vertmax | 97.4% | 99% | 1.6% |

**Does UFC really help in revealing additional faults?**

## Summary – Bonus Task

- UFC > MC/DC 	**FALSE**
- 3 of the 4 case examples at 5% statistical significance
- UFC + MC/DC > MC/DC 	**TRUE**
- 3 of the 4 case examples at 5% statistical significance
- Combine rigorous metrics for assertion coverage and model coverage to measure adequacy of conformance test suites
- UFC metric is sensitive to structure of assertions
- Need assertion coverage metrics that are robust to structure of assertions

## Technology Readiness Level

- “Requirements-Based Test Generation Tool” TRL = 6
- System/subsystem model or prototype demonstration in a relevant environment
- “Validation Adequacy Measurement Tool”  TRL = 6
- System/subsystem model or prototype demonstration in a relevant environment

## Relevance to NASA

- MBD is here - estimate one-half of all NASA missions in development or on the books will use model-based subsystem development
- Extensive use in avionics industry
- How do we know the models are right?
- Model validation problem
- We provide the capability to
- Objectively measure the “quality” of assertion-based black-box validation tests
- Objectively assess the completeness of a model
- Does the model address all assertions?
- Objectively assess the adequacy of a set of assertions
- Are there enough assertions to adequately describe the model?
- Automatically generate truly assertion-based tests

## Achievements to Date

- Formal assertion notation identified
- Most work with LTL
- Extended to work with Live Sequence Charts (LSC)
- Objective validation metrics defined
- Requirements, Antecedent, Unique First Cause, and Unique Cause
- Test case generation tool developed
- Developed tool generating tests from LTL
- Capable of generating tests to all metrics defined
- Prototype tool working on LSC developed
- Developed test-adequacy measurement tool for the defined validation metrics
- Evaluation of metrics and tool
- 12 papers and one PhD dissertation (Ajitha Rajan)

## Next Steps

- Investigate alternative requirements notations to LTL
- Complete empirical evaluation of the effectiveness in model validation
- Flight Guidance Sensor (FGS) evaluation complete
- Display Manager (DM) evaluation in work
- Coordinate evaluation on NASA IV&V project
- Coordinate technology transfer

## Discussion