Model-based testing (MBT) is a variant of testing that relies on explicit behaviour models that encode the intended behaviours of an SUT and/or the behaviour of its environment.

Hierons, R. M., Bogdanov, K., Bowen, J. P., Cleaveland, R., Derrick, J., Dick, J., Gheorghe, M., Harman, M., Kapoor, K., Krause, P., Lüttgen, G., Simons, A. J. H., Vilkomir, S., Woodward, M. R., & Zedan, H. (2009). Using formal specifications to support testing. ACM Comput. Surv., 41 (2), 1-76. URL http://bura.brunel.ac.uk/bitstream/2438/1871/1/landscapes_final.pdf

Dias Neto, A. C., Subramanyan, R., Vieira, M., & Travassos, G. H. (2007). A survey on model-based testing approaches: a systematic review. In Proceedings of the 1st ACM international workshop on Empirical assessment of software engineering languages and technologies: held in conjunction with the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE) 2007, WEASELTech '07, (pp. 31-36). New York, NY, USA: ACM. URL http://www-public.int-evry.fr/\~{}gibson/Teaching/CSC7302/ReadingMaterial/DiasNetoSVT07.pdf

Dias-Neto et al. analyse 271 papers and count more than 219 different MBT approaches that have been proposed, often with associated tools.

This paper helps by developing a taxonomy of six essential dimensions that characterize the different MBT approaches, with examples of how several typical tools fit into that taxonomy. The focus of this paper is on MBT for functional testing, given that this is currently the main industrial usage of MBT. Moreover, the taxonomy is oriented towards users of MBT. It provides a framework for comparing and qualitatively assessing tools and techniques. The perspective on MBT adopted in this paper is inherently bound to the notion of choice: tools generate tests from test models. These test models, by their very nature, do not specify single tests but rather sets of possible tests, and it is up to an MBT tool to choose tests from this set

Dias-Neto A, Subramanyan R, Vieira M, Travassos GH, Shull F. Improving evidence about software technologies: A look at model-based testing. IEEE Software 2008; 25(3):10–13. 8. Pretschner A, Prenninger W, Wagner S, K ¨uhnel C, Baumgartner M, Sostawa B, Z ¨olch R, Stauner T. One evaluation of model-based testing and its automation. Proceedings of the ICSE’05, St Louis, U.S.A., 2005; 392–401. 9. Paradkar A. Case studies on fault detection effectiveness of model based testing generation techniques. Proceedings of the ICSE 2005 Workshop on Advances in Model-based Software Testing (A-MOST’05), St Louis, U.S.A., vol. 30, 2005; 1–7. 10. Horstmann M, Prenninger W, El-Ramly M. Case studies. Model-based Testing of Reactive Systems (Lecture Notes in Computer Science, vol. 3472), Broy M, Jonsson B, Katoen J-P, Leucker M, Pretschner A (eds.). Springer: Berlin, 2005; 439–461. 11. Bernard E, Legeard B, Luck X, Peureux F. Generation of test sequences from formal specifications: GSM 11.11 standard case-study. SW Practice and Experience 2004; 34(10):915–948. 12. Blackburn M, Busser R, Nauman A. Why model-based test automation is different and what you should know to get started. Proceedings of the International Conference on Practical Software Quality and Testing, Washington, DC, U.S.A., 2004. 13. Farchi E, Hartman A, Pinter SS. Using a model-based test generator to test for standard conformance. IBM Systems Journal 2002; 41(1):89–110. 14. Dalal SR, Jain A, Karunanithi N, Leaton JM, Lott CM, Patton GC, Horowitz BM. Model-based testing in practice. Proceedings of the ICSE’99, Los Angeles, U.S.A., 1999; 285–294

A test suite is a finite set of test cases. A test case is a finite structure of input and expected output: a pair of input and output in the case of deterministic transformative systems, a sequence of input and output in the case of deterministic reactive systems, and a tree or a graph in the case of non-deterministic reactive systems. The input part of a test case is called test input.

MBT encompasses the processes and techniques for the automatic derivation of abstract test cases from abstract models, the generation of concrete tests from abstract tests, and the manual or automated execution of the resulting concrete test cases.

The assumption here is that models are specified with languages that are sufficiently precise to allow, in principle, a machine to derive tests from these models

Steps:

1. A model of the SUT is built from informal requirements or existing specification documents. This model is often called a test model, because the abstraction level and the focus of the model are directly linked with the testing objectives. In some cases, the test model could also be the design model of the SUT, but it is important to have some independence between the model used for test generation and any development models, so that errors in the development model are not propagated into the generated tests Validating the model means that the requirements themselves are scrutinized for consistency and completeness, and this often exposes requirements errors. The model must be simpler (more abstract) than the SUT, or at least easier to check, modify, and maintainThe model must be sufficiently precise to serve as a basis for the generation of 'meaningful’ test cases [2 approaches: model as a contract (a priori model) model as a model (a posteriori model)]
2. Test selection criteria are chosen, to guide the automatic test generation so that it produces a ‘good’ test suite—one that fulfills the test policy defined for the SUT. Test selection criteria can relate to a given functionality of the system (requirements-based test selection criteria), to the structure of the test model (state coverage, transition coverage, def–use dataflow coverage), to data coverage heuristics (pairwise, boundary value), to stochastic characterizations such as pure randomness or user profiles, to properties of the environment, and they can also relate to a well-defined set of faults
3. Test selection criteria are then transformed into test case specifications. Test case specifications formalize the notion of test selection criteria and render them operational: given a model and a test case specification, some automatic test case generator must be capable of deriving a test suite.
4. Once the model and the test case specifications are defined, a set of test cases is generated, with the aim of satisfying all the test case specifications The set of test cases that satisfy a test case specification with respect to the model can be empty, in which case the test case specification is said to be unsatisfiable
5. Once the test suite has been generated, the test cases are run. Test execution may be manual—i.e. by a physical person—or may be automated by a test execution environment that provides facilities to automatically execute the tests and record test verdicts

Koomen T, vander Aalst L, Broekman B, Vroon M. TMap Next, for Result-driven Testing. UTN Publishers: Hertogenbosch, The Netherlands, 2006.

Graham D, Veenendaal EV, Evans I, Black R. Foundations of Software Testing: ISTQB Certification. International Thomson Business Press: Stanford, U.S.A, 2008

Model Specification

Scope

Input-only

The input-only models are generally easier to specify, but they have the disadvantage that the generated tests will not be able to act as an oracle. The generated tests may implement an implicit ‘robustness’ oracle, such as checking that the SUT does not crash or throw any exceptions, but they cannot check the correctness of the actual SUT output values, since the model does not specify the expected output values. Input models can be seen as models of the environment. Attacker models in security testing are a prominent example; Markov chains used for statistical testing are a second one.

input/output

the model must be able to predict in advance the expected outputs of the SUT for each input, or at least be able to check whether an output produced by the SUT is allowed by the model or not Philipps J, Pretschner A, Slotosch O, Aiglstorfer E, Kriebel S, Scholl K. Model-based test case generation for smart cards. Proceedings of the 8th International Workshop on Formal Methods for Industrial Critical Systems, 2003

Characteristics

Timing issues: real-time vs. no time

Timing issues are particularly relevant in the large class of real-time systems. Because of the additional degree of freedom, these systems are notoriously hard to test

==== Non deterministic vs. deterministic====

Nondeterminism can occur in the model and/or the SUT. If the SUT exhibits jitter in the time or value domains, this can often be handled when the verdict is built (which might be possible only after all input was applied). If the SUT exhibits genuine nondeterminism, as a consequence of concurrency, for instance, then it is possible that test stimuli as provided by the model depend on prior reactions of the SUT. In these cases, the non-determinism must be catered for by the model, and also by the test cases (they are not sequences anymore, but rather trees or graphs). Finally, nondeterminism in the model can be used for testing deterministic systems. One example is using non-deterministic timeouts to avoid a detailed timing model

Discrete / Hybrid / continuous

Most work in MBT has focused on event-discrete systems, but continuous or hybrid models are often common in many embedded systems

Model paradigm

The third dimension is what paradigm and notation are used to describe the model.

State-based / pre/post notations

Examples of these notations include Z, B, VDM, JML, OCL, and the C#-plus-preconditions used by Spec Explorer

Transition based notations

Typically, they are graphical node-and-arc notations, like FSMs, where the nodes of the FSM represent the major states of the system and the arcs represent the actions or operations of the system

Notations

• FSMs
• statecharts

• UML State machine
• Statemate statechart
• Simulink stateflow charts

• labelled transition systems
• I/O automata

History-based Notations

These notations model a system by describing the allowable traces of its behaviour over time. Message-sequence charts and related formalisms are also included in this group. These are graphical and textual notations for specifying sequences of interactions between components

Functional Notations

system as a collection of mathematical functions functions may be first-order only, as in the case of algebraic specifications, or higher-order, as in notations like HOL

Gaudel, M. C., & Le Gall, P. (2008). Testing data types implementations from algebraic specifications. Formal methods and testing. URL http://arxiv.org/pdf/0804.0970.pdf

Operational Notations

a system as a collection of executable processes, executing in parallel. They are particularly suited to describing distributed systems and communications protocols. Examples include

• process algebras such as CSP or CCS
• Petri net notations.
• hardware description languages like VHDL or Verilog

Stochastic Notations

a system by a probabilistic model of the events and input values and tend to be used to model environments rather than SUT For example, Markov chains - usage profiles

Data-Flow Notations

These notations concentrate on the data rather than the control flow. Prominent examples are Lustre, and the block diagrams of Matlab Simulink, which are often used to model continuous systems.

UML notation offers both a transition-based paradigm, with state machine diagrams, and a pre–post paradigm, with the OCL language Matlab, which models embedded real-time systems using a combination of Simulink block diagrams (a data-flow notation) and Stateflow statecharts (a transition-based notation)

Test selection criteria

facilities that are used to control the generation of tests indirectly define properties of the generated test suites, including their fault detection power, cardinality, complexity It is the task of the test engineer to configure the test generation facilities and choose adequate test selection criteria and test case specifications to meet the project test objectives, e.g. functionality, robustness, security, or performance.

Structural Model Coverage Criteria

These criteria exploit the structure of the model, such as the nodes and arcs of a transition-based model, or conditional statements in a model in pre/post notation For example, when the model uses a pre–post notation, some coverage criteria that are commonly used are: cause–effect coverage, and coverage of all disjuncts in the postcondition. Cause-effect I have a requirement that says: “If A OR B, then C.” The following rules hold for this requirement:

• If A is true and B is true, then C is true.
• If A is true and B is false, then C is true.
• If A is false and B is true, then C is true.
• If A is false and B is false, then C is false

All requirements are translated into nodes and relationships on the cause-effect graph. There are only four possible relationships among nodes, and they are indicated by the following symbols:

• If A always leads to C, there is a black line that connects the nodes.
• If A or B lead to C, there is an “OR” relation.
• If A and B lead to C, there is an “AND” relation.
• If not A leads to C, there is a red line that connects nodes.

The cause-effect graph is then converted into a decision table or “truth table” representing the logical relationships between the causes and effects. Each column of the decision table is a test case. For transition-based models, which use explicit graphs containing nodes and arcs, there are many graph coverage criteria that can be used to control test generation. Some of the coverage criteria commonly used are all nodes (that is, all states), all transitions, all transition pairs, and all cycles

Data Coverage Criteria

These criteria deal with how to choose a few test values from a large data space The basic idea is to split the data space into equivalence classes and choose one representative from each equivalence class

Grindal, M., Offutt, J., & Andler, S. F. (2005). Combination testing strategies: a survey. Software Testing, Verification and Reliability, 15 (3). URL http://csrc.nist.gov/groups/SNS/acts/documents/grindal-offutt-andler.pdf

Kosmatov, N., Legeard, B., Peureux, F., & Utting, M. (2004). Boundary coverage criteria for test generation from formal models. In Software Reliability Engineering, 2004. ISSRE 2004. 15th International Symposium on. IEEE. URL http://kosmatov.perso.sfr.fr/nikolai/publications/kosmatov_issre_2004.pdf

Hamlet D, Taylor R. Partition testing does not inspire confidence. IEEE TSE 1990; 16(12):1402–1411. Duran J, Ntafos S. An evaluation of random testing. IEEE TSE SE 1984; 10(4):438–444. Gutjahr W. Partition testing versus random testing: The influence of uncertainty. IEEE TSE 1999; 25(5):661–674. Nair V, James D, Ehrlich W, Zevallos J. A statistical assessment of some software testing strategies and application of experimental design techniques. Statistica Sinica 1998; 8:165–184

Requirements-Based Coverage Criteria

[informal] For example, if requirement numbers are attached to transitions of a UML state machine or to predicates within the postconditions of a pre–post model, then test generation can aim to cover all requirements

Ad hoc Test Case Specifications

Explicit test case specifications can obviously be used to control test generation. In addition to the model, the test engineer writes a test case specification in some formal notation, and these are used to determine which tests will be generated. For example, they may be used to restrict the paths through the model that will be tested, to focus the testing on heavily used cases, or to ensure that particular paths will be tested Notations commonly used for test objectives include

• UML Sequence diagrams,
• FSMs,
• regular expressions,
• temporal logic formulae,
• constraints,
• Markov chains (for expressing intended usage patterns)

Random and Stochastic Criteria

These are mostly applicable to environment models, because it is the environment that determines the usage patterns of the SUT. The probabilities of actions are modelled directly or indirectly [41, 42]. The generated tests then follow an expected usage profile.

Fault-based Criteria

These are mostly applicable to SUT models, because the goal of testing is to find faults in the SUT. One of the most common fault-based criteria is mutation coverage. This involves mutating the model, then generating tests that would distinguish between the mutated model and the original model. The assumption is that there is a correlation between faults in the model and in the SUT, and between mutations and real-world faults

Andrews, J. H., Briand, L. C., & Labiche, Y. (2005). Is mutation an appropriate tool for testing experiments? In Proceedings of the 27th international conference on Software engineering, ICSE '05, (pp. 402-411). New York, NY, USA: ACM. URL http://www.cs.purdue.edu/homes/jv/510s05/papers/imatt.pdf

Test generation technology

One of the most appealing characteristics of MBT is its potential for automation. Given the test model and some test case specifications, test cases can be derived

Random generation

by sampling the input space of a system Random walks can also be performed on environment models given in the form of (stochastic) usage models, and obviously, this results in certain transition probabilities for the SUT

Prowell, S. J. (2003). Jumbl: A tool for model-based statistical testing. In System Sciences, 2003. Proceedings of the 36th Annual Hawaii International Conference on. IEEE. URL http://www.hicss.hawaii.edu/HICSS36/HICSSpapers/STTCT03.pdf

Search-based algorithms

graph search algorithms such as node or arc coverage algorithms (e.g. the Chinese Postman algorithm [45], which covers each arc at least once), as well as other search-based algorithms such as metaheuristic search, evolutionary algorithms (e.g. genetic algorithms), and simulated annealing

McMinn, P. (2004). Search-based software test data generation: a survey. Software Testing, Verification and Reliability, 14 (2). URL http://philmcminn.staff.shef.ac.uk/publications/pdfs/2004-stvr.pdf

(Bounded) model checking

is a technology for verifying or falsifying properties of a system. For certain classes of properties, model checkers can yield counterexamples when a property is not satisfied. The general idea of test case generation with model checkers is to first formulate test case specifications as reachability properties, for instance, ‘eventually, a certain state is reached, or a certain transition fires’ (e.g. [47, 48]). A model checker then, by searching for counterexamples for the negation of the property, yields traces that reach the given state or that eventually make the transition fire. Other variants use mutations of models or properties to generate test suites.

Offutt A, Liu S, Abdurazik A, Ammann P. Generating test data from state-based specifications. Journal of Software Testing, Verification and Reliability 2003; 13(1):25–53. Hong H, Lee I, Sokolsky O, Ural H. A temporal logic based theory of test coverage and generation. Proceedings of the TACAS’02, 2002; 327–341.

Symbolic execution

runs an (executable) model not with single input values but with sets of input values (e.g. [49–51]). These are represented as constraints. In this way, symbolic traces are generated: one symbolic trace represents many fully instantiated traces. The instantiation to concrete values must obviously be performed in order to get test cases for a SUT. Symbolic execution is guided by test case specifications. Often enough, these boil down to reachability statements as in the case of model checking. In other cases, test case specifications are given as explicit constraints, and the symbolic execution is guided by having to respect these constraints

Pretschner A. Classical search strategies for test case generation with constraint logic programming. Proceedings of the Formal Approaches to Testing of Software, Aalborg, Denmark, 2001; 47–60.

Marre B, Arnould A. Test sequences generation from LUSTRE descriptions: GATEL. Proceedings 15th IEEE Conference on Automated Software Engineering, Grenoble, France, 2000; 229–237.

Colin S, Legeard B, Peureux F. Preamble computation in automated test case generation using constraint logic programming. Journal of Software Testing, Verification and Reliability 2004; 14(3):213–235.

Deductive theorem proving

Dick J, Faivre A. Automating the generation and sequencing of test cases from model-based specifications. Proceedings of the 1st International Symposium of Formal Methods Europe, Odense, Denmark, vol. 670, 1993; 268–284.

Helke S, Neustupny T, Santen T. Automating test case generation from Z specifications with Isabelle. Proceedings of the 10th International Conference on Z Users, Reading, U.K., vol. 1212, 1997; 52–71.

with provers that support the generation of witness traces or counterexamples. One variant is similar to the use of model checkers where a theorem prover replaces the model checker. Most often, however, theorem provers are used to check the satisfiability of formulas that directly occur as guards of transitions in state-based models. A theorem prover can compute assignments for the variables that occur in the guards and that, in turn, give rise to values of the respective input and output signals. A sequence of such sets of signals then becomes the test case

Constraint solving

is useful for selecting data values from complex data domains, e.g. in combinatorial n-wise testing. It is also often used in conjunction with other methods such as symbolic execution, graph search algorithms, model-checking or theorem proving [54, 55] where specific relationships between variables in guards or conditions are expressed as constraints and efficiently solved by dedicated constraint solvers.

Test execution

Test execution is done either online or offline from the test generation

Online test execution

With online testing, the test generation algorithms can react to the actual outputs of the SUT. This is sometimes necessary if the SUT is non-deterministic, because the test generator can see which path the SUT has taken, and follow the same path in the model (Section 3.2).

Offline test execution

Offline testing means that test cases are generated strictly before they are run. Offline test generation from a non-deterministic model is more difficult, and involves creating test cases that are trees or graphs rather than sequences.

Advantages of offline testing,

when applicable, are directly connected to the generation of a test repository.

• The generated tests can be managed and executed using existing test management tools, which means that fewer changes to the test process are required. One can generate a set of tests once, then execute it many times on the SUT (e.g. regression testing).
• test generation and test execution can be performed on different machines or in different environments, as well as at different times
• Test suites can be split and applied to many SUTs in parallel
• It is also possible to perform a separate test minimization pass over the generated test suite, to reduce the size of the test set
• Moreover, testing real-time systems may be impossible if test generation is too time-consuming.
• if the test generation process is slower than test execution, then there are obvious advantages into doing the test generation phase just once

Manual execution

Manual test execution means that a human tester executes each generated test case by interacting with the SUT, following the instructions in the test case

Automated test execution

automated test execution means that the generated test is already an executable test script of some form

CLASSIFICATION OF TOOLS

[typically a table]

AETG (Automatic Efficient Test Generator)

Cohen, D. M., Dalal, S. R., Fredman, M. L., & Patton, G. C. (1997). The AETG system: An approach to testing based on combinatorial design. Software Engineering, IEEE Transactions on, 23 (7). URL http://testingeducation.org/BBST/testdesign/Cohen_AETG_System.pdf

model-based test input generator for combinatorial testing

To reduce the number of generated test inputs, it uses a pair-wise algorithm to ensure that all combinations of the data values for each pair of variables are tested. It also supports all-triples or all-quadruples testing

The oracle for each test input has to be provided manually

generates tests for offline manual execution

http://www.pairwise.org/

JUMBL - J Usage Model Builder Library

academic model-based statistical testing tool

statistical usage-based models using Markov chains, the analysis of models, and the generation of test cases

it is a model of the expected environment and is input data only

Models are untimed and discrete

a transition-based notation for describing Markov chain usage models

random and statistical test selection criteria (based on the transition arc probability of the usage model)

Automated generation of test inputs using statistical search algorithms and the Markov model

Offline

Microsoft Spec Explorer

It provides a model editing, composition, exploration, and visualization environment within Visual Studio, and can generate offline .NET test suites or execute tests as they are generated (online). Other examples of commercial MBT tools that use behavioural test models are Qtronic from Conformiq [58] and CertifyIt from Smartesting [59]

The input model of Spec Explorer is a SUT input–output model, which is typically composed from several simpler models. The model provides the oracle for each generated test case.

State-based models are written in C# (extended with preconditions), and a regular expression notation is used to specify history-based (trace-based) models/scenarios. The C# models can have internal state and parameterized methods with complex parameters.

several strategies for managing the exploration of the model, including data coverage of parameter values and the state space (the state space can be restricted by several grouping and slicing techniques), and structural model criteria such as covering all transitions

It uses algorithms similar to bounded model checking to explore the model and generate tests

It supports both online and offline testing

related work

Broy M, Jonsson B, Katoen J-P, Leucker M, Pretschner A (eds.). Model-based Testing of Reactive Systems (Lecture Notes in Computer Science, vol. 3472). Springer: Berlin, 2005.