MBT with Test Model Analysis


Origin: Brian Nielsen / Aalborg University, completed by Wolfgang Herzner / AIT

Written: July 2014

Purpose: Increase confidence in generated tests by analysing (model-checking) the model from which tests are generated (valid tests that satisfy requirements, failing tests likely caused by wrong implem.).

Context/Pre-Conditions: Model-based test case generation (MBTCG) is used as described by pattern ‘MBT’.

To consider:

– It depends on chosen modelling language/notation how easy and efficiently this pattern can be applied.

– Test (modelling) experts need some expertise in model checking.



Participants and Important Artefacts

Only those are described here that operate in addition to those described in pattern ‘MBT’.

Analysis objectives: Properties that have to be possessed by the test model. They are derived from requirements by the T&A model engineer, and should be formulated such that they can be proven by model checking. Additional properties are generic checks like alle edges/locations reachable, abscense of deadlocks.

Model analyser: Process that examines whether the test models meets the analysis objectives. A typical technique used here is model checking.


Actions / Collaborations

Only those are described here that operate in addition to those described in pattern ‘MBT’.

(1) The T&A model engineer defines the analysis objectives from the requirements, perhaps in cooperation with the customer.

(2) The model-analyser is usually a model checking process (controlled by a human expert) that examines the model whether it meets an objective or it find a counter example (path through the model) that violates the objective.



Benefits: Successfull checking of analysis objectives increases trust in correction of subsequently generated test cases significantly. In particular:

– if a test case fails it can (most likely) be assumed that the implementation is wrong,

– if a test case passes confidence is high that the implementation actually conforms to the requirements.


– Model checking is expensive with respect to memory and CPU time, and may fail for more complex test models.


– Of course, if model checking shows that the model violates an objective, it should be corrected. This is indicated by the dashed path in the structure diagram.

– If model checking fails for a certain analysis objective, AT-pattern “Use-test run to slice model” could help.


Application Examples

MBAT Automotive Use Case 1 (Brake by Wire) / Scenarios 2 (Analysis on the Analysis Model) and 5 (TCG based on Test Model)

Participants / Tools:


Tools: ViTAL (MDH); Farkle (Enea/XDIN/ALTEN)

MBAT Automotive Use Case 8 (Virtual Prototype Airbag ECU) / Scenarios 1-4:

Participants / Tools:

Analysis of Objectives

– The T&A model is checked for internal consistency with MoMuT::REQs.

– The T&A model, which was generated with UPPAAL, is verified against formal expressions entered by the verification engineer in order to validate this T&A model. Thereby also generic model properties like absence of deadlocks are analyzed.

Model Analysis

– MoMuT::REQs


MBAT Aerospace Use Case 4 (Flight Management System/UAV) / Scenarios 2 (Analysis and test for “system architecture” validation) and 3 (System testing validation):

Participants / Tools:

Create T&A model: Analysis Model: ALES FSV-BCL Toolbox, Test Model: ELVIOR TestCast Generator

Model Analysis: ALES FSV-Formal Verification

Model based Test Generator: ELVIOR TestCast Generator

Executor: ELVIOR Test Cast TTCN-3 (SC02) + AAEM Test environment (SC03)

Formalized requirements: SYSML requirement model: AAEM

Test model: SYSML statechart for POF functionality: AAEM

Test objectives: List of test criteria: ELVIOR TestCast Generator

Analysis objectives: List of derived requirements

Test suite: Selenium WebDriver

Adaptor+harness: TTCN3 functions: ELVIOR TestCast generator (SC02) + Executor to AAEM test environment adaptor: AMET (SC03)

SUT / Model generated executable: on host (C code): AAEM (SC02)

SUT / Real system executable: on OBMC board (C code): AAEM (SC03)

Report: Test results, analysis verdicts + counter examples: ALES + ELVIOR

MBAT Rail Use Case 1 (Automatic Train Control) / Scenario 2 (System Validation – Create and check T&A model):

Participants / Tools:

Create T&A model: MaTeLo Editor

Model Analysis: Model checking MaTeLo

Model based Test Generator: MaTeLo Editor & MaTeLo Testor

Executor: Mastria 200 Sol (In-house simulator)

Inspect Verdicts: ODEP + TARAM (In-house strip and analysis tools)

Comments: Model analysis is based on model checking function of MaTelo, it doesn‘t examine whether the test models meets the analysis objectives. It checks only some points, namely:

– The “Invoke” and “Terminate” state number.

– No outgoing transitions on the “Terminate” state.

– No entering transition on the “Invoke” state.

– A state is not a destination of duplicated transitions.

– For each profile chosen in the model checking, test if the sum of probabilities at the transitions leaving a state equals 1.0.


Relations to other Patterns

Pattern Name Relation*
MBT This pattern complements (extends) MBT
Use Test Run to Slice Model If the model is too large for analysis, that pattern can help to split test model such that parts can be analysed
Model and Refinement Checking Both use same methods
MBA-Based Runtime Behaviour Verification Also analyses the test model, but for generating test cases rather than for assuring model correctness

* “this pattern” denotes the pattern described here, “that pattern” denotes the related pattern