Introduction to Model-Based Testing¶
Software quality is a matter of increasing importance and growing concern. Systematic testing plays an important role in the quest for improved quality and reliability of software systems. Software testing, however, is often an error-prone, expensive, and time-consuming process. Estimates are that testing consumes 30-50% of the total software development costs. The tendency is that the effort spent on testing is still increasing due to the continuing quest for better software quality, and the ever growing size and complexity of systems. The situation is aggravated by the fact that the complexity of testing tends to grow faster than the complexity of the systems being tested, in the worst case even exponentially. Whereas development and construction methods for software allow the building of ever larger and more complex systems, there is a real danger that testing methods cannot keep pace with these construction and development methods, so that these new systems cannot sufficiently fast and thoroughly be tested anymore. This may seriously hamper the development and testing of future generations of software systems.
Model-Based Testing (MBT) is one of the
technologies to meet the challenges imposed on software testing. With
MBT a System Under Test (
sut) is tested against an abstract model of
its required behaviour. This model serves as the system specification
and is the starting point for testing. It prescribes what the
sut should, and what it should not do, that is, the behaviour of
sut shall conform to the behaviour prescribed in the model. The
model itself is assumed to be correct and valid; it is not the direct
subject of testing or validation.
The main virtue of MBT is that the model is a perfect basis for the generation of test cases, allowing test automation that goes well beyond the mere automatic execution of manually crafted test cases. MBT allows for the algorithmic generation of large amounts of test cases, including test oracles for the expected results, completely automatically, from the model of required behaviour. Moreover, if this model is valid, i.e., expresses precisely what the system under test should do, all these generated tests are provably valid, too.
From an industrial perspective, model-based testing is a promising approach to detect more bugs faster and cheaper. The current state of practice is that test automation mainly concentrates on the automatic execution of tests, but that the problem of test generation is not addressed. Model-based testing aims at automatically generating high-quality test suites from models, thus complementing automatic test execution.
From an academic perspective, model-based testing is a formal-methods approach to testing that complements formal verification and model checking. Formal verification and model checking intend to show that a system has specified properties by proving that a model of that system satisfies these properties. Thus, any verification is only as good as the validity of the model on which it is based. Model-based testing, on the other hand, starts with a (verified) model, and then aims at showing that the real, physical implementation of the system behaves in compliance with this model. Due to the inherent limitations of testing, such as the limited number of tests that can be performed in a reasonable time, testing can never be complete: ”testing can only show the presence of errors, not their absence” [R24].
Benefits of model-based testing¶
Model-based testing makes it
possible to generate test cases automatically, enabling the next step in
test automation. It makes it possible to generate more, longer, and more
diversified test cases with less effort, whereas, being based on sound
algorithms, these test cases are provably valid. Since a model specifies
both the possibe stimuli (inputs) to the
sut and the allowed
responses (outputs), the generated test cases contain inputs to be
provided to the
sut as well as outputs expected from the
which leads to better test oracles and less misinterpretation of test
Creating models for MBT usually already leads to better understanding of system behaviour and requirements and to early detection of specification and design errors. Moreover, constructing models for MBT paves the way for other model-based methods, such as model-based analysis, model checking, and simulation, and it forms the natural connection to model-based system development that is becoming an important driving force in the software industry.
Test suite maintenance, i.e., continuously adapting test cases when systems are modified, is an important challenge of any testing process. In MBT, maintenance of a multitude of test cases is replaced by maintenance of a model. Also diagnosis, i.e., localizing the fault when a failure is detected, is facilated through model-based diagnostic analysis. Finally, various notions of (model-) coverage can be automatically computed, expressing the level of completeness of testing, and allowing better selection of test cases.
Altogether, MBT is a promising approach to detect more bugs faster and cheaper, and thus to improve the quality and reliability of the system under test.
Sorts of model-based testing¶
There are different kinds of testing, and thus of model-based testing, depending on the kind of models being used, the quality characteristics being tested, the level of formality involved, the degree of accessibility and observability of the system being tested, and the kind of system being tested. Here, we consider model-based testing as formal, specification-based, active, black-box, functionality testing of reactive systems.
It is testing, because it involves checking some properties of the
sut by systematically performing experiments on the real, running
sut. as opposed to, e.g., formal verification, where properties are
checked on a model of the system. The kind of properties being checked
are concerned with functionality, i.e., testing whether the system
correctly does what it should do in terms of correct responses to given
stimuli. as opposed to, e.g., performance, usability, reliability, or
maintainability properties. Such classes of properties are often
referred to as quality characteristics [R41].
We do specification-based, black-box testing. The
sut is seen
as a black box without internal detail, which can only be accessed and
observed through its external interfaces, as opposed to white-box
testing, where the internal structure of the
sut, i.e., the code, is
the basis for testing. The externally observable behaviour of the system
is compared with what has been specified in the model.
The testing is active, in the sense that the tester controls and
sut in an active way by giving stimuli and triggers to
sut, and observing its responses, as opposed to passive testing,
or monitoring. Our
sut s are dynamic, data-intensive, reactive
systems. Reactive systems react to external events (stimuli, triggers,
inputs) with output events (responses, actions, outputs). In dynamic
systems, outputs depend on inputs as well as on the system state.
Data-intensive means that instances of complex data structures are
communicated in inputs and outputs, and that state transitions may
involve complex computations and constraints.
Finally, we deal with formal testing: the model, which serves as
specification prescribing the desired behaviour is written in some
formal language with precisely defined syntax and semantics. Moreover,
there is a formal, well-defined theory underpinning these models,
sut s, tests, and their relations, in particular, the correctness
sut s with respect to models, and the validity of
tests with respect to models. This enables formal reasoning about
soundness and exhaustiveness of test generation algorithms and the
generated test suites, i.e., that tests exactly test what they should
In another form of model-based testing, called statistical model-based
testing, models do not prescribe required behaviour of the
they describe how users use a system. Such models are called
statistical usage profiles, operational profiles, or customer
profiles. The idea is that tests are selected based on the expected
usage of the
sut, so that behaviours that are more often used, are
more thoroughly tested [R55]. Such models are derived from usage
information such as usage logs. Statistical model-based testing enables
the comprehensive field of statistics to be used with the goal of
assessing the reliability of systems.
Theory for model-based testing¶
A theory for model-based testing
must, naturally, first of all define the models that are considered. The
modelling formalism determines the kind of properties that can be
specified, and, consequently, the kind of properties for which test
cases can be generated. Secondly, it must be precisely defined what it
means for an
sut to conform to a model. Conformance can be
expressed using an implementation relation, also called conformance
relation [R17]. Since the
sut is considered as a black box, its
behaviour is unknown and we cannot construct a model that precisely
describes the behaviour of the
sut, yet, we do assume that such a
model, though unknown, exists in a domain of implementation models. This
assumption is commonly referred to as the testability hypothesis, or
test assumption [R31]. The testability hypothesis allows reasoning
sut s as if they were formal models, and it makes it possible
to define the implementation relation as a formal relation between the
domain of specification models and the domain of implementation models.
Soundness of test suites, i.e., do all correct
sut s pass, and
exhaustiveness, i.e., do all incorrect
sut s fail, are defined with
respect to an implementation relation.
In the domain of testing reactive systems there are two prevailing
‘schools’ of formal model-based testing. The oldest one uses
Mealy-machines, also called finite-state machines (FSM); see [R18] [R47],
51]. Here, we concentrate on the other one that uses labelled
transition systems (LTS) for modelling. A labelled transition system is
a structure consisting of states with transitions, labelled with
actions, between them. The states model the system states; the labelled
transitions model the actions that a system can perform. There is a rich
and well-understood theory for MBT with LTS, which is elaborated in
Sect. 3. Other approaches to MBT for non-reactive systems include
abstract-data-type based testing [R7] and property-based testing, of
which the tool
QuickCheck is the prime example [R19]. Originally
Haskell, property-based testing is now applied for
Labelled transition systems form a well-defined semantic basis for modelling and model-based testing, but they are not suitable for writing down models explicitly. Typically, realistic systems have more states than there are atoms on earth (which is approximately 10 50) so an explicit representation of states is impossible. What is needed is a language to represent large labelled transition systems. Process algebras have semantics in terms of labeled transition systems, they support different ways of composition such as choice, parallelism, sequencing, etc., and they were heavily investigated in the eighties [R50] [R39] [R42]. They are a good candidate to serve as a notation for LTS models.
Model-based testing challenges¶
Software is anywhere, and ever more systems depend on software: software controls, connects, and monitors almost every aspect of systems, be it a car, an airplane, a pacemaker, or a refrigerator. Consequently, overall system quality and reliability are more and more determined by the quality of the embedded software. Typically, such software consists of several million lines of code, with complex behavioural control-flow as well as intricate data structures, with distribution and a lot of parallelism, having complex and heterogeneous interfaces, and controlling diverse, multidisciplinary processes. Moreover, this software often comes in many variants with different options and for different platforms. It is continuously evolving and being modified to adapt to different environments and new user requirements, while increasing in size, complexity, connectivity, and variability. Software is composed into larger systems and systems-of-systems, whereas system components increasingly originate from heterogeneous sources: there can be legacy, third-party, out-sourced, off-the-shelf, open source, or newly developed components.
For model-based testing, these trends lead to several challenges. First, the size of the systems implies that making complete models is often infeasible so that MBT must deal with partial and under-specified models and abstraction, and that partial knowledge and uncertainty cannot be avoided. Secondly, the combination of complicated state-behaviour and intricate input and output-data structures, and their dependencies, must be supported in modelling. Thirdly, distribution and parallelism imply that MBT must deal with concurrency in models, which introduces additional uncertainty and non-determinism. In the fourth place, since complex systems are built from sub-systems and components, and systems themselves are more and more combined into systems-of-systems, MBT must support compositionality, i.e., building complex models by combining simpler models. Lastly, since complexity leads to an astronomical number of potential test cases, test selection, i.e., how to select those tests from all potential test cases that can catch most, and most important failures, within constraints of testing time and budget, is a key issue in model-based testing.
In short, to be applicable to testing of modern software systems, MBT shall support partial models, underspecification, abstraction, uncertainty, state & data, concurrency, non-determinism, compositionality, and test selection. Though several academic and commercial MBT tools exist, there are not that many tools that support all of these aspects.
Model-based testing tools¶
Model-based testing activities are too
laborious to be performed completely manually, so, for MBT to be
effective and efficient, tool support is necessary. A large number of
MBT tools exist, as a Web-search will immediately show.
one of these MBT tools.
TorXakis is a proof-of-concept, research tool that is being
developed by the Radboud University Nijmegen, the University of Twente,
and ESI (TNO) in the Netherlands. It is an on-line (on-the-fly) MBT tool
for formal, specification-based, active, black-box, functionality
testing of reactive systems, rooted in the ioco-testing theory for
labelled-transition systems [R61] [R62]. It implements the ioco-test
generation algorithm for symbolic transition systems [R30], and it uses a
process-algebraic modelling language
Txs inspired by the language
LOTOS [R11] [R42], which is supplemented with an algebraic data-type
specification formalism, for which rewriting and SMT solvers are used
for calculation and manipulation [R22]. Moreover,
with most of the challenges posed in the previous paragraph: it supports
modelling of state-based control flow together with complex data, it
deals with non-determinism, abstraction, partial models and
under-specification, concurrency, and composition of complex models from
TorXakis supports state & data but no
probabilities, real-time, or hybrid systems. Test selection is primarily
random, but guidance can be provided using test purposes.
TorXakis is an experimental MBT tool, used in (applied) research,
education, and industrial case studies and experiments.
TorXakis currently misses good usability, scalability does not
always match the requirements of complex systems-of-systems, and more
sophisticated test selection strategies are necessary but these are
being investigated [R14].
Current MBT algorithms and tools can potentially generate many more tests from a model than can ever be executed. Consequently, test selection is one of the major research issues in model-based testing. Test selection concerns the problem of finding criteria for selecting from the astronomical number of potential test cases those tests that have the largest chance of detecting most, and the most important bugs, with the least effort. Random approaches, which are often used for small systems, do not suffice for large and complex systems: the probability of completely randomly selecting an important test case within the space of all possible behaviours converges to zero. At the other end from random there is the explicit specification of test purposes, i.e., a tester specifies explicitly what she wishes to test, but that requires a lot of manual effort, and, moreover, how should the tester know what to test. Different approaches have been identified for determining what the “most important behaviours” are, such as testing based on system requirements, code coverage, model coverage, risk analysis, error-impact analysis, or expected user behaviour (statistical usage profiles, or operational profiles).
Related to apriori test selection, is aposteriori coverage, quality, and
confidence in the tested system. Since exhaustive testing is practically
impossible, the question pops up what has been achieved after testing:
can the coverage of testing, the quality of the tested
sut, or the
confidence in correct functioning of the
sut, somehow be formalized
and quantified? It is not to be expected that these fundamental research
questions will soon be completely solved.
MBT is an interesting technique once a model of the
available. Availability of behavioural models, however, is one of the
issues that currently prohibits the widespread application of MBT. In
the first place, there is the question of making and investing in
models: there is reluctance against investing in making models, being
considered as yet another software artifact. Secondly, mastering the art
of behavioural modeling requires education and experience that is not
always available. Thirdly, the information necessary to construct a
model, in particular for legacy, third-party, or out-sourced systems or
components, is not always (easily) available.
These issues lead to the question whether models can be generated
automatically, e.g., for use in regression testing or testing systems
after refactoring. Model generation from an
sut, a kind of black-box
reverse engineering, (re)constructs a model by observing the behaviour
sut, either passively from system logs, or actively by
performing special tests. This activity is called model learning, also
known as testbased modeling, automata learning, or grammatical
inference, and it is currently a popular research topic [R65].
New software testing methodologies are needed if testing shall keep up with software development and meet the challenges imposed on it, otherwise we may not be able to test future generations of systems. systems. Model-based testing may be one of them.