# Efficient Dynamic Model Based Testing

P. Spaendonck

► To cite this version:

P. Spaendonck. Efficient Dynamic Model Based Testing. 43th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2023, Lisbon, Portugal. pp.173-188, 10.1007/978-3-031-35355-0_11. hal-04731931

HAL Id: hal-04731931

https://inria.hal.science/hal-04731931v1

Submitted on 11 Oct 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
<figure><img src="image_2.png" /></figure>

ifip

International Federation for Information Processing

This document is the original author manuscript of a paper submitted to an IFIP
conference proceedings or other IFIP publication by Springer Nature. As such, there
may be some differences in the official published version of the paper. Such
differences, if any, are usually due to reformatting during preparation for publication or
minor corrections made by the author(s) during final proofreading of the publication
manuscript.
# Efficient Dynamic Model Based Testing
Using Greedy Test Case Selection

P. H. M. van Spaendonck(✉) ID

Department of Mathematics and Computer Science, Eindhoven University of
Technology, Eindhoven, The Netherlands

P.H.M.v.Spaendonck@tue.nl

**Abstract.** Model-based testing (MBT) provides an automated approach for finding discrepancies between software models and their implementation. If we want to incorporate MBT into the fast and iterative software development process that is Continuous Integration Continuous Deployment, then MBT must be able to test the entire model in as little time as possible.

However, current academic MBT tools either traverse models at random, which we show to be ineffective for this purpose, or use precalculated optimal paths which can not be efficiently calculated for large industrial models. We provide a new traversal strategy that provides an improvement in error-detection rate comparable to using precalculated paths. We show that the new strategy is able to be applied efficiently to large models. The benchmarks are performed on a mix of real-world and pseudo-randomly generated models. We observe no significant difference between these two types of models.

**Keywords:** model based testing · test case selection · efficient testing

## 1 Introduction

Testing has become a core tenet of modern-day software engineering. It has been repeatedly shown that having thoroughly tested software leads to higher quality software with significantly lower maintenance and development costs [3, 5]. This has led to test-driven engineering, in which tests for a component or feature are written before its actual implementation commences, and the implementation is deemed to be correct only once all tests succeed.

Similarly, we see a rise in the usage of model-driven engineering, in which software components are first described on a higher level of abstraction as a state machine/model. Model-based techniques can then be used to deliver correct and verified software. For example, in [4], UMLsec models are used to verify that the security requirements of a single-sign-in software application are correctly enforced.

Model-Based Testing (MBT), such as the ioco-based approach originally outlined in [14] by Tretmans, sits at the intersection of these two engineering

This publication is part of the PVSR project (with project number 17933) of the MasCot research programme which is financed by the Dutch Research Council (NWO).
approaches and allows us to use an abstract model to automatically test its
implementation. The ability to automatically generate tests makes MBT very
useful for software development by, in theory, removing the need to spend time
manually writing tests. In practice, however, the exhaustive approach of MBT
can easily lead to testing the same behavior multiple times. This contrasts with
manually written test suites which are often designed to have as little overlap in
tested behavior as possible. Reducing the overlap in tested behavior when using
MBT should thus be considered a critical step for applying it for the testing of
large complex systems.

The focus of our research is reducing overlap in tested behavior when apply-
ing the ioco-based MBT technique. For this technique, we confine ourselves to
discrete datatypes and we formalize systems as directed graphs in which edges
can be labeled with inputs or outputs that use these datatypes. As such, a
test run through the model should have as little overlap with itself as possible.
Visiting the same part of the model multiple times means that the behavior
corresponding to that part of the model would also be tested multiple times.

In [6], van den Bos and Tretmans provide a possible solution to reducing this
overlap by automatically calculating test paths that cover all symbolic transi-
tions of a given model. The MBT tool then uses an SMT solver to calculate
concrete values for the queries while traversing the pregenerated path. Their
approach shows a significant speedup over the classic random test-case selec-
tion approach when used to detect non-conformances in several mutants of the
Bounded Retransmission Protocol [8].

However, calculating such a global optimal path is NP-hard and thus becomes
computationally too expensive when applied to large industrial systems. Another
issue, which van den Bos and Tretmans also acknowledge, is that using the same
test path every time might cause the test to miss bugs that do not present
themselves along the given path [6]. Likely because of these reasons, academic
MBT tools, such as TorXakis [15], opt to traverse the model at random instead.

We investigate whether a simple and straightforward greedy test-case selec-
tion strategy can be used to attain a similar speedup to the one attained through
the usage of pre-generated paths, whilst also being able to be applied to large
models. For the initial comparison, we use our greedy strategy to run the same
experimental setup used for the global optimal strategy in [6], i.e. mutation
detection on the Bounded Retransmission Protocol [8]. Our greedy strategy per-
forms 8.2 times better than the random strategy according to the arithmetic
mean.

Second, we test the scalability of the greedy solution by applying it to large
real-world models, as well as randomly generated statespaces of varying sizes.
These random statespaces are approximations of complex systems running under
run-to-completion semantics. The greedy strategy provides a noticeable speedup
over the random test-case selection strategy when aiming to cover at least 70%
of the states of the given models. We also observe that the generated models
provide similar results to those of the real-life use case.
In Sect. 2, we briefly discuss related work on model-based testing techniques and optimizations. In Sect. 3, we give the underlying formalization of the theory of ioco-based MBT. In Sect. 4, we discuss the algorithm used for ioco-based MBT. In Sect. 5, we discuss our new optimizations. In Sect. 6, we show and discuss our benchmarks. We give our final conclusion and discuss other areas of research that might be important for the usage of MBT within the software development cycle in Sect. 7.

## 2 Related Work

When formalizing systems as abstract models, we often prefer abstracting away over data and formalizing them as discrete datatypes, as this significantly reduces the complexity of the system. However, when formalizing low-level cyber-physical components, we see that the exact value of data, e.g. the angle of an air-intake vent, can not be abstracted away over, as they are central to the correctness of such components. In such cases, systems can be formalized as continuous or hybrid automata [10]. We highlight some of the state-of-the-art test optimization techniques used for systems with continuous data.

For systems with continuous data, MBT is done through search-based testing in which meta-heuristics, such as genetic algorithms or simulated annealing, are used to automatically generate test data. Reducing overlap in tested behavior can, in these instances, be reformulated as an optimization problem. As an example, in [2], meta-heuristics are used to find optimal inputs that maximize the distance between the expected optimal input, thus increasing the likelihood of a fault occurring, and between previous inputs, decreasing the possible overlap with previously tested behavior. In [12], a combination of dimensionality reduction and surrogate modeling techniques based on supervised learning is used to scale up similar techniques to be able to be applied to the incredibly large search spaces encountered within the cyber-physical domain of the automotive industry.

The systems that we describe in Sect. 3 and use throughout the paper, are models with discrete datatypes, often with no direct interrelation. As such, there is no continuous search space to optimize over and the test case selection comes down to optimizing the traversal of the graph that is the specification model. However, these two techniques are not exclusive, and can very well be combined, such as is shown in [11], in which search-based techniques are used to pick viable candidates for the data parameters of functions.

Last, we discuss work on reducing overlap in tested behavior when using online, i.e. a finite test suite is generated a priori, model-based conformance testing techniques. In [7], Cartaxo et al. provide a solution to reducing overlap in tested behavior by measuring the similarity of different tests in the generated test suite and picking a subset of tests such that the similarity measure between the tests in the subset is as low as possible. By doing so, they are able to reduce the number of run tests with 80% while still maintaining a similar fault detection rate to that of a full run test suite. In [1], Aichernig et al. use model-based
mutation testing in which mutant models i.e. models containing faulty behavior, are generated from the correct specification model, which, in turn, are used to generate tests aimed at detecting the faults contained in the mutant models. Aichernig et al. use a bounded equivalence checker to find and remove identical mutants that would lead to tests being generated with an overlapping tested behavior. Offline MBT techniques, such as the one used by us, are generally more suited for testing behavior that only occurs after long specific sequences of inputs and outputs.

# 3 Theory of Model Based Testing

In this section, we give the theory needed to understand how the behavior of a given system is formalized, and how these formal models are used during dynamic MBT. The MBT theory presented here is the same as the original theory described in [14] with only some notational differences.

The expected behavior of a system is expressed as an input-output labeled transition system (IOLTS), a variation of labeled transition systems in which the action labels are split into disjoint input- and output-action sets. We define an IOLTS as follows:

**Definition 1.** An IOLTS $L$ is defined as the 5-tuple $L = (Q, q_0, A_I, A_O, \rightarrow)$, where:

- $Q$ is the finite set of states,

- $q_0 \in Q$ is the initial state,

- $A_I$ and $A_O$ are the sets of input- and output-actions, respectively, such that $A_I \cap A_O = \emptyset$ and $\tau, \delta \notin A_I \cup A_O$.

- $\rightarrow \subseteq Q \times (A_I \cup A_O \cup \{\tau, \delta\}) \times Q$ is the transition relation, such that $\langle q, \delta, q' \rangle \in \rightarrow$ iff $q = q'$ and the state $q$ has no outgoing transitions labeled with an output action $a_{out} \in A_O$ or $\tau$-action.

Given states $p, q$, and some action label $a$, we use the shorthand notation $p \xrightarrow{a} q$ instead of $\langle p, a, q \rangle \in \rightarrow$.

In the set of actions $A_I \cup A_O$, each element corresponds to a function in the implementation. We make a distinction between input actions $A_I$, functions that we call as inputs to the system, and output actions $A_O$, functions of other components that can either trigger as a response to inputs given to the system, or spontaneously, e.g. by some internal timer timing out.

We further extend our set of actions with the special actions $\tau$ and $\delta$. The $\tau$-action represents an externally non-observable action, e.g. some internal calculation that occurs as a result of calling a function. The $\delta$-action, referred to as quiescence, represents the system remaining idle. A transition with a $\delta$-action occurs exactly in all states in which it is not possible to take an output transition nor an internal action and must be a self-loop, i.e. the begin- and endpoint must be the same.

For readability, we write $A_\delta$ as shorthand for $A_I \cup A_O \cup \{\delta\}$ and we write $A$ as shorthand for $A_I \cup A_O$.
During MBT, a sequence of actions referred to as a *suspension trace*, is used to keep track of the actions performed thus far. We define the set of suspension traces using Definitions 2, and 3.

**Definition 2.** Let $L = \langle Q, q_0, A_I, A_O, \rightarrow \rangle$ be an IOLTS. We define the observable path relation $\Rightarrow \subseteq Q \times A_\delta^* \times Q$ as the smallest relation satisfying:

- $q \stackrel{\epsilon}{\Rightarrow} q$ given any state $q \in Q$, where $\epsilon$ refers to the empty sequence,

- given states $q, q', q'' \in Q$ and some word $w \in A_\delta^*$, if $q \xrightarrow{\tau} q'$ and $q' \xrightarrow{w} q''$ then $q \xrightarrow{w} q''$, and

- given states $q, q', q'' \in Q$, an observable action $a \in A_\delta$, and a word $w \in A_\delta^*$, if $q \xrightarrow{a} q'$ and $q' \xrightarrow{w} q''$ then $q \xrightarrow{aw} q''$.

**Definition 3.** Let $L = \langle Q, q_0, A_I, A_O, \rightarrow \rangle$ be some IOLTS. Given a state $q \in Q$, the set of suspension traces straces($q$) $\subseteq A_\delta^*$ is defined as follows:

$$ \text{straces}(q) = \{w \in A_\delta^* | \exists q' \in Q [q \xrightarrow{w} q']\}. $$

Model Based Testing tests whether the behavior of the implementation conforms to the behavior of the specification, i.e. the implementation never gives an output that the specification does not allow. This conformance is described using the **input-output-conformance relation ioco** on IOLTSs, originally defined in [14], and is given in Definition 5.

**Definition 4.** Let $L = \langle Q, q_0, A_I, A_O, \rightarrow \rangle$ be an IOLTS. We define the mappings $out_L: P(Q) \rightarrow P(A_O)$ and $L \textbf{ after} : A_\delta^* \rightarrow P(Q)$ as follows:

- given some set of states $qs \subseteq Q$, we have

$$ out_L(qs) = \{a_{out} \in A_O | \exists q \in qs, q' \in Q [q \xrightarrow{a_{out}} q']\}, \text{ and} $$

- given some suspension trace $\sigma \in \text{straces}(q_0)$, we have

$$ L \textbf{ after } \sigma = \{q \in Q | q_0 \xrightarrow{\sigma} q\}. $$

**Definition 5.** Given an IOLTS $L_{impl}$ of the implementation and an IOLTS $L_{spec} = \langle Q, q_0, A_I, A_O, \rightarrow \rangle$ of the specification, the conformance $L_{impl} \textbf{ ioco } L_{spec}$ holds iff given any trace $\sigma \in \text{traces}(q_0)$, we have

$$ out_{L_{impl}}(L_{impl} \textbf{ after } \sigma) \subseteq out_{L_{spec}}(L_{spec} \textbf{ after } \sigma). $$

# 4 The MBT Algorithm

We now discuss the MBT algorithm from [14], for which we give a pseudocode description in Algorithm 1. The MBT algorithm uses the set $qs$, which initially contains the initial state $q_0$ and all states reachable from there using only $\tau$-actions, to keep track of which states it could be in at the start of each iteration.
<caption>**Algorithm 1: MBT algorithm**</caption>

**Data:** A specification IOLTS $L = \langle Q, q_0, A_I, A_O, \rightarrow \rangle$ and a timeout time $t$.
1 $qs \leftarrow \{q \in Q | q_0 \stackrel{\delta}{\rightarrow} q\}$
2 **while** next($L, qs$) $\neq \emptyset$ **do**:
3 **do either:**
4 &nbsp;&nbsp;&nbsp;&nbsp;**if** next($L, qs$) $\cap$ $A_I \neq \emptyset$ **then**:
5 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**select** $a_{in}$ **from** next($L, qs$) $\cap$ $A_I$
6 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**send**($a_{in}$)
7 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**qs** $\leftarrow \{q \in Q | \exists q' \in qs : q' \stackrel{a_{in}}{\Rightarrow} q\}$
8 **or**:
9 &nbsp;&nbsp;&nbsp;&nbsp;**try** $a_{out} \leftarrow rcv(t)$
10 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** $a_{out} \in next(L, qs)$ **then**:
11 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**q** $\leftarrow \{q \in Q | \exists q' \in qs : q' \stackrel{a_{out}}{\Rightarrow} q\}$
12 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**else**:
13 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**return** false
14 &nbsp;&nbsp;&nbsp;&nbsp;**on** timeout:
15 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** $\delta \in next(L, qs)$ **then**:
16 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**qs** $\leftarrow \{q \in qs | q \stackrel{\delta}{\rightarrow} q\}$
17 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**else**:
18 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**return** false

We define next($L, qs$) to be the set of possible actions that can be taken from at least one state in $qs$, i.e. $next(L, qs) = \{a \in A_\delta | \exists q \in qs, q' \in Q [q \stackrel{a}{\rightarrow} q']\}$.

The function send($a$) on line 6 causes the implementation to execute the function corresponding to the input action $a$. Whenever the implementation calls a function corresponding to some output action $a_{out}$, the label $a_{out}$ is sent back to the MBT algorithm and added to a response queue. Messages in the queue are read first-in-first-out using the rcv($t$) function on line 9, removing the read message in the process. If rcv($t$) is called and the queue is empty, it will wait till a new message is received. If no message is received within the timeout time $t$, the function throws a timeout.

The algorithm repeatedly does one of two things:

- Some input action $a_{in}$ that is possible from any state in $qs$ is picked and the implementation is requested to execute the corresponding function using send($a_{in}$). The tool then updates the set of possible states $qs$ accordingly and continues.

- The MBT tool listens for a possible output action $a_{out}$ using rcv($t$). If an action is received, we verify whether it is an allowed action. If the action is allowed, the set of states $qs$ is updated accordingly and we continue. If $a_{out}$ is not a possible action from any state in $qs$, then we can conclude that the implementation is not ioco with the specification model, and the test has failed. If no response is received within the timeout time $t$, we assume the implementation to be idle/quiescent. The algorithm reduces the set $qs$ to only the quiescent states in $qs$, i.e. states with a $\delta$-loop. If none of the states in $qs$
are quiescent, then the implementation is also not ioco with the specification model, and the test has failed.

Note that the MBT algorithm does not terminate if no behavioral differences are ever detected. The tester must decide when to terminate. The termination criterion that is used throughout the paper is state coverage, i.e. the percentage of states that have been reached/tested throughout the run.

# 5 The Greedy Test Case Selection Strategy

To reduce the amount of overlap in tested behavior, we want to avoid querying inputs leading to already tested states. However, calculating a global optimal path, i.e. finding the shortest path visiting each state at least once, is too computationally expensive to be done on complex systems which have a large number of states. Instead, our proposed strategy intends to approximate the global optimal path by picking locally optimal solutions. This is done by, calculating all possible paths originating from our current set of states qs, of a given length n, and then picking the input action corresponding to the path with the least states that have already been visited. If more than one such action is available, a random contender is picked.

We make use of two optimizations to reduce the amount of work required to find these local-optimal paths. To highlight the need for these optimizations, let us consider an IOLTS in which each state has, on average, $\lambda$ outgoing transitions. Simply calculating all possible paths of length n and picking the most optimal one, would still be in the order of $O(|qs| \cdot \lambda^n)$.

For the first optimization, we note that once an optimal path of length n has been found, and a singular action has been performed, it is unnecessary to reconsider all possible paths of length n, since we already have a near-optimal path of length $n - 1$. Instead, we only consider the extensions of our leftover path. In Definition 6 we outline the path-tree data structure that we use to keep track of the previously performed calculations.

**Definition 6.** Given an IOLTS $L = \langle Q, q_0, A_I, A_O, \rightarrow \rangle$, a path-tree is a 6-tuple $pt = \langle a, q, next, d, v, v_{max} \rangle$, where

- we have projection functions `a`, `q`, `next`, `d`, `v` and `vmax` defined on `pt` such that `a(pt) = a`, `q(pt) = q`, `next(pt) = next`, `d(pt) = d`, `v(pt) = v`, and `vmax(pt) = v_{max}`,

- `a` is an action label leading to state `q`, i.e. $\exists q' \in Q [q' \xrightarrow{a} q]$,

- `next` is a set of path-trees such that $\forall pt' \in next[q \xrightarrow{a(pt')} q']$,

- `d` is the depth of the tree, i.e. 1 plus the highest depth among the path-trees in next,

- `v`, i.e. the value of a path-tree, equals the maximum amount of unvisited states that can be reached through a sequence of `d` transitions, starting with the transition $q' \xrightarrow{a} q$, and

- $v_{max}$ is used to store the maximum value among the path-trees in next.
<table><caption>**Algorithm 2:** The *grow*(*L*, *pt*, *n*) algorithm for path-trees</caption>
  <thead>
    <tr>
      <th></th>
      <th>Data:</th>
    </tr>
  </thead>
  <tbody>
    <tr>
      <td>1</td>
      <td>The IOLTS L = &lt;Q, q<sub>0</sub>, A<sub>I</sub>, A<sub>O</sub>, →&gt;, a path-tree<br/>pt = &lt;a, q, next, d, v, v<sub>max</sub>&gt;, and a target depth of n ≥ d.</td>
    </tr>
    <tr>
      <td>2</td>
      <td>if d = n :</td>
    </tr>
    <tr>
      <td>3</td>
      <td>return;</td>
    </tr>
    <tr>
      <td>4</td>
      <td>else if next = &emptyset;:</td>
    </tr>
    <tr>
      <td>5</td>
      <td>for a:A, q':Q s.t. q &rarr; q' do:</td>
    </tr>
    <tr>
      <td>6</td>
      <td>add &lt;a, q', &emptyset;, 1, covered(q'), 0&gt; to next</td>
    </tr>
    <tr>
      <td>7</td>
      <td>for pt' ∈ next do:</td>
    </tr>
    <tr>
      <td>8</td>
      <td>if v(pt') + (&lt;(n &minus; 1)&minus; d(pt')&gt;) ≥ v<sub>max</sub>:</td>
    </tr>
    <tr>
      <td>9</td>
      <td>grow(L, pt', n &minus; 1)</td>
    </tr>
    <tr>
      <td>10</td>
      <td>v<sub>max</sub> &larr; max(v<sub>max</sub>, v(pt'))</td>
    </tr>
    <tr>
      <td>11</td>
      <td>v &larr; v<sub>max</sub> + covered(q)</td>
    </tr>
    <tr>
      <td>12</td>
      <td>d &larr; n</td>
    </tr>
  </tbody>
</table>

We now discuss the *grow* function outlined in Algorithm 2, which extends a given path-tree *pt* = ⟨*a*, *q*, *next*, *d*, *v*, *v*<sub>max</sub>⟩ to depth *n*. The *covered* function, that is used on lines 5 and 10, returns 1 if the state *q* has not been visited yet, and otherwise returns 0. If the target depth *n* and path-tree depth *d* are equal, then no further calculations will be necessary and we immediately terminate (line 1 and 2). Otherwise, we first check whether *next* is empty, i.e. no calculations belonging to this path-tree have been performed past the state *q*. If *next* is empty, a new path tree of depth 1 is inserted for each transition originating from the state *q* (lines 3 through 5). The *grow* function is then called recursively on each path-tree in *next* using a target depth of *n* − 1, and the variables *d*, *v* and *v*<sub>max</sub> are updated accordingly (lines 6 and 8 through 11).

<figure><img src="image_3.png" /><figcaption>**Fig. 1.**
Preemptive termination example</figcaption></figure>

The **if** statement on line 7 corresponds to our second optimization which consists of pre-emptively terminating the calculation of a given path when we can determine that it will no longer be able to beat or the value of the current optimal path candidate. For example, take Fig. 1 in which a part of a partially explored IOLTS is shown. For readability, the transition labels have been left out and previously visited states have been colored gray. The MBT algorithm is currently in state 0 and wants to find an optimal path of length 3. It first calculates a possible path of length 3 along state 1 and finds a possible path containing 2 unvisited states. It then calculates a path along state 4 but after seeing that the first two states, i.e. 4 and 5, have already been visited, the calculation is terminated since we can determine that the path along state 4 can not contain 2 or more unvisited states.

To use the greedy test-case selection strategy we make use of a variable *paths* to store our current set of path trees originating from *qs* and replace the statement on line 5 of the MBT algorithm shown in Algorithm 1 with the
**Algorithm 3:** The greedy test case selection strategy.

**Data:** The IOLTS $L$, the set of currently maintained path-trees *paths*, the set of current states *qs*, the target depth of *n*, and a set of possible actions *options*.

1. **pick_input**($L, paths, qs, n, options$) :=

2. paths $\leftarrow \{pt \in paths \mid a(pt) \in options\}$

3. **if** paths = $\emptyset$ :

4. **for** $q \in qs$ **do**:

5. **for** $a \in options, q' \in Q$ **s.t.** $q \xrightarrow{a} q'$ **do**:

6. **insert** $\langle a, q', \emptyset, 1, covered(q'), 0 \rangle$ **in** paths

7. $v_{best} \leftarrow 0$

8. $pref \leftarrow \emptyset$

9. **for** $pt \in paths$ **do**:

10. **grow**($L, pt, n$)

11. **if** $v(pt) > v_{best}$ :

12. $v_{best} \leftarrow path.v$

13. $pref \leftarrow \{a(pt)\}$

14. **else if** $v(pt) = v_{best}$ :

15. **insert** $a(pt)$ **in** $pref$

16. **return** $pref$

following statement:

select $a_{in}$ from pick_input($L, paths, qs, n, next(L, qs) \cap A_I$).

The *pick_input* function is given in Algorithm 3 and takes care of growing all current path-trees to the target depth *n*, and reducing the set of possible input actions *options* to the ones belonging to a local-optimal path of length *n*. Whenever some action *a* is performed by the implementation, i.e. an action *a* is sent to or received from the implementation, the set of paths *paths* is updated to the union of *next* of all path trees whose action equals *a*. This allows us to reuse the already performed calculations.

## 6 Benchmarking Results

We split up our benchmarks into two sets. In Sect. 6.1, we test whether our greedy strategy shows improvements over the random test case selection strategy similar to those of the global optimal solution provided in [6]. This is done by benchmarking our strategy to the same set of benchmarks used for the global optimal solution. In Sect. 6.2, we benchmark the scalability of our solution by using both the greedy and the random strategy on a variety of large and complex generated and real-world models.

For both sets of benchmarks, we are interested in the number of transitions each traversal strategy needs to reach a certain goal. For the first set, this goal is detecting non-conformance and for the second set, this goal is a specific percentage of state coverage. We measure the number of transitions instead of the
amount of time required, since the throughput, i.e. the number of transitions per second, is largely dependent on the quiescence time, which can vary greatly per system.

The systems that we look at in both sections are deterministic and internal-choice, i.e. in each state, it is possible to query inputs to the implementation or receive outputs from the implementation.

## 6.1 Fault Detection Speed

The benchmarks used in [15] come from the automata wiki [13], which is an online repository containing various formalized models that can be used for benchmarking. One set of these models pertains to the Bounded Retransmission Protocol [8] by Philips. For this communication protocol, the Wiki provides both a formalization of its intended behavior, as well as 6 mutants. This protocol is a variation of the alternating-bit protocol and provides ordered and partially reliable communication for a sequence split into three messages over a possibly unreliable communication channel. As such, a sequence of messages will always arrive in a clearly marked sequencing, however, the transmission of the entire sequence is terminated if the transmission of a given message has failed a fixed number of times. Each of the six mutants represents incorrect implementations of the communication protocol. We refer the reader to the wiki [13] for exact explanations of the differences between the mutants and the correct implementation.

As was done in [6], we measure the average amount of transitions required to find a non-conformance caused by each mutation using MBT for both the random strategy and our greedy strategy. For each strategy, the average is calculated over a total of 100 runs per mutant. The averages of these runs, as well as the results by van den Bos and Tretmans [6], are shown in Table 1. For reference, the last two columns contain the original benchmarks, where switch coverage is their global optimal solution and TorXakis is the symbolic random test case selection strategy. Since our tool does not allow for infinite data types, the variables representing the three messages have been replaced with constants. As such, we could not properly capture mutant six, since it makes assertions about the three messages that are used, and we omit this mutant from our benchmarks. We calculate the arithmetic mean of the averages of all 5 experiments for each test case selection strategy.

We observe a significant difference in the average detection speed when testing mutant 2 or 6. In mutant 2, the number of permitted failed transmissions after which communication is terminated is reduced from 5 to 4. In mutant 5, an incorrect final response message is sent if only the first 2 messages have been transmitted correctly. Both mutations require a very specific sequence of inputs to become observable and, as the probability of such a specific sequence being picked at random is very low, the random test case selection strategies require significantly longer to observe these mutants.

We observe that the greedy strategy performs ≈ 8.2 times better than the random (non-symbolic) strategy. With the exclusion of Mutant 6, the global
optimal solution actually performs ≈ 20.6 times better than the random (symbolic) strategy instead of the ≈ 7.7 times improvement that occurs when Mutant 6 is included. The original authors note that the decreased performance of the global optimal strategy applied to Mutant 6 is caused due the lack of randomness in deciding which values to use for the message variables. Therefore, we believe that the slight randomness of the greedy strategy would lead to similar performance results as those of random test case selection strategies and the performance improvement should stay the same as it is now if Mutant 6 were added to the set of benchmarks.

<table><caption>**Table 1.** Average number of transitions required to different detect mutations of the Bounded Transmission Protocol through MBT using greedy test case selection, a priori generated path [6], and random test case selection</caption><thead><tr><th rowspan="2"></th><th colspan="2">Explicit data (2.9k states)</th><th colspan="2">Symbolic data (6 states)</th></tr><tr><th>greedy w. N = 5</th><th>random</th><th>A Priori</th><th>TorXakis</th></tr></thead><tbody><tr><td>Mutant 1</td><td>20</td><td>22</td><td>44</td><td>12</td></tr><tr><td>Mutant 2</td><td>95</td><td>412</td><td>16</td><td>234</td></tr><tr><td>Mutant 3</td><td>16</td><td>21</td><td>8</td><td>12</td></tr><tr><td>Mutant 4</td><td>27</td><td>29</td><td>6</td><td>18</td></tr><tr><td>Mutant 5</td><td>180</td><td>2280</td><td>18</td><td>1620</td></tr><tr><td>Mutant 6</td><td>-</td><td>-</td><td>164</td><td>76</td></tr><tr><td>mean</td><td>67.6</td><td>552.8</td><td>42.7</td><td>328.7</td></tr></tbody></table>

## 6.2 Applicability on Large Models

To investigate the effectiveness of our strategy when used on large systems, we measure the average amount of transitions required by both our greedy strategy and the random strategy, to cover a given percentage of states on such large models. These measurements are performed on both real-world models as well as generated models. We opt to also generate representative models since acquiring a large variety of large complex industrial models is rather difficult. The generated models are based on previous research by Groote et al. [9], in which random LTSs are generated and are shown to be representative of real-world models. This is done by comparing fault-detection results to real-life models and statistical analysis.

The models generated in [9], are generated as follows: An LTS with *N* states is generated, and each state is given *λ* outgoing transitions with the target states being uniformly distributed. This process is repeated *p* times, after which all *p* random LTSs are parallel composed. The resulting model is then used as a representative LTS.

The models which we generate, are meant to be representative of systems under run-to-completion semantics which dictates that once a system has begun processing some input, it will not start processing another input until the first
input has been fully processed, even if both inputs could be processed simultane-
ously. These semantics are very useful as they significantly reduce the complexity
of a model, both in terms of state-space as well as in terms of cognitive com-
plexity.

Since we can see the processing of a given input as a single monolithic action,
we end up with similar-looking models to the aforementioned generated LTSs.
We thus decide to generate our models as follows: We generate *p* LTSs as was
done before, each transition is labeled with some label representing an arbitrary
input action followed by an arbitrary sequence of *r* output action that forms
the processing of the input action. Once all *p* processes have been parallelly
composed, the singular transitions are replaced with a sequence of transitions,
labeled with the corresponding input action and the sequence of *r* output actions.

We require the resulting IOLTS to be deterministic and to be fully connected, i.e. there is always some path from each state to any other state. Using deterministic IOLTSs simplifies the problem situation, reduces variation during testing, and allows us to focus solely on the efficient traversal of the given model. The fully-connected requirement is imposed such that it is always possible to eventually test all states. Intuitively, a system that would not meet this requirement would favor an intelligent strategy that can avoid taking wrong transitions, i.e. a transition that causes yet untested states to become unreachable, in favor of the at-random approach.

We implemented an LTS simulator, that mimics the behavior of the model,
and use this as the implementation for all of our benchmarks since we are only
interested in the exploration of our LTS. This eliminates a significant portion of
the time spent on running the implementation and communication between this
and the tool.

For our first set of benchmarks, we apply MBT on the model of an industrial
component from Philips. This component is part of the larger set of software
used on the Philips Azurion, a large and complex x-ray machine that allows for
live imaging during critical heart-surgery operations. Fig. 2 shows the results of
these benchmarks. The benchmarks consist of 10 runs per strategy. The average
of these runs is indicated by the dashed line (—). The dotted lines (···) show
the average plus/minus the standard deviation of these runs. We see that the
greedy strategy requires ≈ 6 times fewer steps than the random strategy to
cover 90% of the states of the model at Philips. We note that the model contains
transitions that, once traversed, cause certain states to no longer be reachable.
As such, the random strategy could not consistently test more than ≈ 90% of
the states.

For our second set of benchmarks, we use a subsystem of a large Dezyme
specification of a sorting robot. This model is part of the set of example models
that come with the Dezyme tool, and we believe that, while being an example
model, it is representative of machinery that can be encountered in the real
world. The model is composed of a large set of modeled subcomponents and,
as a result of this, consists of approximately 220 000 states. Since exploring
such a large model would take a considerable amount of time, we use statespace
<figure><img src="image_4.png" /><figcaption>**Fig. 2.** Number of transitions required to achieve given percentages of state coverage of the model at Philips by both the greedy and random strategies</figcaption></figure>

reduction techniques to reduce its size whilst still maintaining all of the behavior. To do so, we make all quiescence labels explicit and then reduce our LTS modulo branching-bisimulation equivalence. This reduces the model from 220 000 states to only 617 states.

Figure 3 shows the results of the benchmarks performed on the Dezyne sorting machine and shows the greedy strategy requiring ≈ 5 times fewer transitions than the random strategy to cover 95% of the sorting machine model. The benchmarks consist of 10 runs per strategy. The average of these runs is indicated by the dashed line (—). The dotted lines (...) show the average plus/minus the standard deviation of these runs.

For our final set of benchmarks, we apply both strategies to several randomly generated statespaces. All random statespaces are generated using the aforementioned technique. We used three different sets of generation parameters. Each set of parameters was used to generate 3 random statespaces. Each randomly generated statespace was then used to perform 10 separate runs per strategy. The set of benchmarks thus consists of 30 runs per strategy per set of generation parameters. The statespaces used for the top-left benchmark are generated using the parameters $N = 10, \lambda = 6, r = 1$, and $p = 2$. The statespaces used for the top-right benchmark are generated using the parameters $N = 10, \lambda = 6, r = 1$, and $p = 3$. The statespaces used for the bottom benchmark are generated using the parameters $N = 800, \lambda = 6, r = 1$, and $p = 1$.
<figure><img src="image_5.png" /><figcaption>**Fig. 3.** Number of transitions required to achieve given percentages of state coverage of the sorting machine model by both the greedy and random strategies</figcaption></figure>

<figure><img src="image_6.png" /><figcaption>**Fig. 4.** Number of transitions required to achieve given percentages of state coverage of several generated statespaces</figcaption></figure>

Figure 4 shows the results of the benchmarks performed on the generated statespaces. The greedy strategy, on average, required ≈ 5.5× fewer transitions than the random strategy to reach 98.75% of all states, significantly fewer transitions on the much larger statespaces that were used in the top-right benchmarks,
and ≈ 4.2× fewer transitions on the non-parallel statespaces used for the bottom benchmarks. All of the benchmarks showcase similar improvements over the old random strategy.

# 7 Conclusion and Future Work

We conclude that our greedy solution is a significant improvement over the old at-random exploration strategy when we want to thoroughly test complex systems using dynamic MBT. Our strategy has shown to have a significant speedup over the random strategy when applied to both the industrial model and the sorting machine, as well as the large set of generated statespaces.

However, how often we can query the tested implementation within a given timeframe still remains to be a big bottleneck for MBT. And we believe this to be an important area for future research if we want to be able to efficiently use MBT in software development. More future work lies in studying non-fully connected models, in which a wrong decision could cause a significant portion of states to no longer be visitable. One might propose to solve this, by allowing the test suite to reset the system. Resetting real-world systems is however time-consuming, and thus knowing when to trigger a reset could be crucial in speeding up testing. Another interesting aspect of such systems is finding and comparing strategies that aim to maximize the possible state coverage, by avoiding such wrong decisions.

# References

1. Aichernig, B.K., Jöbstl, E., Tiran, S.: Model-based mutation testing via symbolic refinement checking. Sci. Comput. Program. **97**, 383–404 (2015). https://doi.org/10.1016/j.scico.2014.05.004. Special Issue: Selected Papers from the 12th International Conference on Quality Software (QSIC 2012)

2. Araujo, H., Carvalho, G., Mousavi, M.R., Sampaio, A.: Multi-objective search for effective testing of cyber-physical systems. In: Ölveczky, P.C., Salaün, G. (eds.) SEFM 2019. LNCS, vol. 11724, pp. 183–202. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30446-1_10

3. Beck, K.: Test-Driven Development: By Example. Addison-Wesley Professional, Boston (2003)

4. Best, B., Jurjens, J., Nuseibeh, B.: Model-based security engineering of distributed information systems using UMLsec. In: 29th International Conference on Software Engineering (ICSE 2007), pp. 581–590 (2007). https://doi.org/10.1109/ICSE.2007.55

5. Bhat, T., Nagappan, N.: Evaluating the efficacy of test-driven development: industrial case studies. In: Proceedings of the 2006 ACM/IEEE International Symposium on Empirical Software Engineering, ISESE 2006, pp. 356–363. Association for Computing Machinery, New York (2006). https://doi.org/10.1145/1159733.1159787

6. van den Bos, P., Tretmans, J.: Coverage-based testing with symbolic transition systems. In: Beyer, D., Keller, C. (eds.) TAP 2019. LNCS, vol. 11823, pp. 64–82. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-31157-5_5
7. Cartaxo, E., Machado, P., de Oliveira Neto, F.: On the use of a similarity function for test case selection in the context of model-based testing. Softw. Test. Verif. Reliab. **21**, 75–100 (2011). https://doi.org/10.1002/stvr.413

8. Groote, J.F., van de Pol, J.: A bounded retransmission protocol for large data packets. In: Wirsing, M., Nivat, M. (eds.) AMAST 1996. LNCS, vol. 1101, pp. 536–550. Springer, Heidelberg (1996). https://doi.org/10.1007/BFb0014338

9. Groote, J.F., van der Hofstad, R., Raffelsieper, M.: On the random structure of behavioural transition systems. Sci. Comput. Program. **128**, 51–67 (2016). https://doi.org/10.1016/j.scico.2016.02.006. https://www.sciencedirect.com/science/article/pii/S0167642316000599. Special issue on Automated Verification of Critical Systems (AVoCS’14)

10. Henzinger, T.A.: The Theory of Hybrid Automata. In: Inan, M.K., Kurshan, R.P. (eds.) Verification of Digital and Hybrid Systems, pp. 265–292. Springer, Heidelberg (2000). https://doi.org/10.1007/978-3-642-59615-5_13

11. Lefticaru, R., Ipate, F.: Functional search-based testing from state machines. In: 2008 1st International Conference on Software Testing, Verification, and Validation, pp. 525–528 (2008). https://doi.org/10.1109/ICST.2008.32

12. Matinnejad, R., Nejati, S., Briand, L., Brcukmann, T.: Mil testing of highly configurable continuous controllers: scalable search using surrogate models. In: Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering, ASE 2014, pp. 163–174. Association for Computing Machinery, New York (2014). https://doi.org/10.1145/2642937.2642978

13. Neider, D., Smetsers, R., Vaandrager, F., Kuppens, H.: Benchmarks for automata learning and conformance testing (2019). https://doi.org/10.1007/978-3-030-22348-9_23

14. Tretmans, J.: Model based testing with labelled transition systems. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) Formal Methods and Testing. LNCS, vol. 4949, pp. 1–38. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78917-8_1

15. Tretmans, J., van de Laar, P.: Model-based testing with torxakis. In: Central European Conference on Information and Intelligent Systems, pp. 247–258 (2019). https://www.proquest.com/conference-papers-proceedings/model-based-testing-with-torxakis/docview/2366658121/se-2