Use Test Run to Slice Test Model

Meta-Information

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

Written: October 2014

Purpose: Rule out further defects along known failing or suspect test by analysis. Relevant when model was too large to be completely analysed.

Context/Pre-Conditions: Model-based test case generation (MBTCG) with model analysis is used as described by pattern “MBT with Test Model Analysis”.

To consider:

– Experience is needed to apply this pattern.

– There exist test cases generated from model which fail with some suspect that the implementation is not wrong.

.

Structure

Participants and Important Artefacts

Only those are described here that operate in addition to those described in pattern “MBT with Test Model Analysis”.

Model slicer: (Experts guarded) process that reduces test model (by further abstraction) or extracts a submodel that can be checked for the analysis objectives that could not be verified on the full model. Two automatic types of slicers are envisioned.

.

Actions / Collaborations

Only those are described here that operate in addition to those described in pattern “MBT with Test Model Analysis”‘, or behave differently as described there.

(1) Applying the model analyser with respect to a certain analysis objective fails in that no conclusion can be drawn due to insufficient computation resources.

(2) Test cases are generated anyway, in particular those that examine the analysis objective or corresponding requirements, respectively.

(3) If a test case fails or a suspect behavior is observed, the test trace is forwarded to the “model slicer”.

(4) The model slicer reduces the model (at least its state space) by removing parts not relevant for the test case. Potential techniques for achieving these are:

Projection along the observable behavior of the trace: The observed input/output behavior from the trace is considered a particular scenario in which the model behavior is examined. This can be achieved by using the scenario as environment for the SUT model, or by projecting the communication between the original environment model and SUT-model on the abstracted observable events in the trace, hence only exploring this scenario. The resulting model may still potentially highly non-deterministic with a large state-space.

“Warm up” the model: Use the test trace to bring the model into the state where the trace leaves the model, and start model-checking there. This new, presumably interesting, state is used as new initial state.

.

Discussion

Benefit:

– Increases the trust gained in the test model of „MBT with Test Model Analysis“ where its model-checking process cannot cope with the test model.

Limitation:

– Needs more experience.

Comments:

– If test cases are not generated from model, check that error trace /failing test is valid for the model.

.

Relations to other Patterns

Pattern Name	Relation*
MBT with Test Model Analysis	This pattern can help that pattern if model checking the test model fails for due to model complexity (e.g. state space explosion)
Find Reduction Rules for MBT	Similar scope (reducing model complexity

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