Coverage Completion for MBTCG
Meta-Information
Also known as Increase TCG Coverage by Analysis
Origin: Brian Nielsen / Aalborg University, (restructured partially by Wolfgang Herzner (AIT)
Written: July 2014
Purpose: The intent of this pattern is to improve the coverage obtained in a test suite that likely has incomplete model and code coverage, because it has been generated through the use of simulation, random, or manual test generation requirements based test generation.
Context/Pre-Conditions: Model-based test case generation: A test model in a suitable (analyzable) notation and the SUT exist.
To consider: A model-checker may not be able to generate test cases for all missing coverage items: some may be infeasible, and some may not be found by the model-checker due to state-explosion. Similarly Path synthesis may not guarantee coverage due to the path explosion problem in symbolic executions. The model-checker and path synthesis tools are advanced tools that may require tuning of their parameters to work optimally. Also they may require significant execution resources.
Structure
Participants and Important Artefacts
(Simulation based) Test Generator: The TCG tool performs simulation exploration of the model to generate test cases in a way that it cannot guarantee coverage of the model a-priori.
Model Coverage Analyzer: takes as input an existing test suite generated from the model (or at least “compatible with the model”) and compares the model coverage that can be achieved after execution (assumes deterministic models, see discussion) for a given criterion, and produces a report of covered and uncovered coverage items.
A Model-checker: is a formal analysis tool that performs systematic (and potentially exhaustive) state space exploration of a model and formal logical property, and outputs a verdict for each property, and possibly a witness trace (or counter example trace) of how the property may be satisfied on the model.
Test Executer and Coverage Evaluator: executes the test cases in a suite one by one, and outputs a report of the verdict of the test executions together with a code coverage report for particular chosen criterion.
Path Synthesizer: performs symbolic execution and is capable of computing the program path (and its pre-condition) for a given program point to be executed (in a deterministic program).
A Test Oracle: is capable for a given test input vector to define what the correct output vector (response) of the system should be.
.
Actions / Collaborations
(1) The workflow starts from a given test model, from which an initial test suite is generated.
(2) Then the coverage of the generated test suite is analyzed at the model level against the chose coverage criterion.
(3) For each missing coverage item, a logical property is formulated to the model-checker, which is then invoked. It is assumed that the model-checker is able to run batches of properties in the same execution instance, otherwise it must be invoked for each coverage item. The witness traces are used as test cases (this may require some adaptation similar to that done by the test case generator). When all properties have been checked (or allocated execution time or memory has been exhausted) no further witnesses can be found, and this branch of the workflow terminates.
(4) The generated test suite is executed of the SUT, and the obtained coverage measured by a code-level metric.
(5) The missing coverage items are fed to the path synthesizes which tries to identify a program path to each missing item and compute their precondition (and concrete instance input vectors) thereof.
(6) The test oracle (assumed to be a test engineer) defines the required output vector or system response for an input, and combines them into a test case. When done, the workflow ends.
.
Discussion
– The pattern could be sub-divided into two patterns, one for model coverage, and one for code coverage: however, it is here joined because the recommended flow is to target model coverage (test all specified behavior) before code coverage (test implemented behavior), see [MBAT D_WP2.1_2_1, 2013].
– There may be special circumstances where the manual oracle step can be automa-ted and the test model can be used instead. However, this requires that SUT and model “interfaces” match and an automated mapping can be established between generated data input vectors at code level and input signals at model level. In this case the oracle can be inferred from the model via a model-based test generation tool or (symbolic) execution of the model, given the generated input vector.
– There exists model-based TCG tools that a-priori tries to achieve a given coverage criteria. These tools are often based on analysis engines like model-checkers to perform systematic state space exploration.
– There are numerous coverage criteria defined for models and code. The pattern here is agnostic about the specific criterion used.
– Perhaps the pattern should be re-defined to let the model-analyzer run after test case execution? This may help with non-deterministic models.
.
Application Examples
MBAT Aerospace Use Case 7 (Flight Guidance System):
Participants / Artefacts:
Test Generator: MaTeLo
Model Coverage Analyzer: Diversity
Model Checker: Diversity
Test Executer and Coverage Evaluator: PathCrawler
Path Synthesizer: PathCrawler
Test Oracle: (Diversity)
Comment: code-level MC/DC coverage is required by several industry standards, but hard to address at model level. The pattern is used to find possible completions of test models in the case where the tests which are automatically generated from the test model do not achieve MC/DC coverage.
MBAT Rail Use Case 1 (Automatic Train Control) / SC02 (System Validation):
Participants / Artefacts:
Test Generator: MaTeLo Testor
Model Coverage Analyzer: Artimin (CEA)
Model Checker: MaTeLo
Test Executer and Coverage Evaluator: Mastria 200Sol
Test Oracle: MaTeLo & Python Convertor
Comment: Python convertor adapts expected results generated by MaTelo to Alstom format.
MBAT Rail Use Case 2 (Rapid Transit Metro System by Ansaldo STS):
Participants / Tools:
Test Generator: Test scripts are generated starting from high-level system description (Out Of Scope of MBAT project)
Model Coverage Analyzer: ALES Formal Specs Verifier (FSV)
Model-checker: FSV
Test Executer and Coverage Evaluator:: FSV (code lines)
Path Synthesizer: FSV
Test Oracle: (Out Of Scope of MBAT project)
Comment: The outputs of tests are verified and the test coverage report is generated (Out Of Scope of MBAT project). Then, the paths not covered by dynamic tests are formalized as rules to be verified, in order to automatically identify the inputs needed to cover those paths or to demonstrate that the corresponding states cannot be reached.
MBAT Aerospace Use Case 6 (TALARION by EADS IW):
Participants / Tools:
Test Generator: sepp.med MBTSuite and BTC ATG
Model Coverage Analyzer: manually (future: IBM MoV)
Model-checker: IBM MoV
Test Executer and Coverage Evaluator:: own test environment
.
Relations to other Patterns
| Pattern Name | Relation |
| MBT | MBT is the general pattern for MBTCG and test case application |