∎

11institutetext: Wen-ling Huang 22institutetext: University of Bremen
Department of Mathematics and Computer Science
22email<EMAIL_ADDRESS>33institutetext: Jan Peleska 44institutetext:
(Corresponding author)
University of Bremen
Department of Mathematics and Computer Science
44email<EMAIL_ADDRESS>

# Complete Requirements-based Testing with Finite State Machines††thanks:
Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research
Foundation) – project number 407708394.

Wen-ling Huang  Jan Peleska

###### Abstract

In this paper, new contributions to requirements-based testing with
deterministic finite state machines are presented. Elementary requirements are
specified as triples consisting of a state in the reference model, an input,
and the expected reaction of the system under test defined by a set of
admissible outputs, allowing for different implementation variants. Composite
requirements are specified as collections of elementary ones. Two
requirements-driven test generation strategies are introduced, and their fault
coverage guarantees are proven. The first is exhaustive in the sense that it
produces test suites guaranteeing requirements satisfaction if the test suite
is passed. If the test suite execution fails for a given implementation,
however, this does not imply that the requirement has been violated. Instead,
the failure may indicate an arbitrary violation of I/O-equivalence, which
could be unrelated to the requirement under test. The second strategy is
complete in the sense that it produces test suites guaranteeing requirements
satisfaction if and only if the suite is passed. Complexity considerations
indicate that for practical application, the first strategy should be
preferred to the second. Typical application scenarios for this approach are
safety-critical systems, where safety requirements should be tested with
maximal thoroughness, while user requirements might be checked with lesser
effort, using conventional testing heuristics.

###### Keywords:

Property-based testing Requirements-driven testingModel-based testing
Guaranteed fault coverage Finite state machines

††offprints: Jan Peleska

##  1 Introduction

###  1.1 Background: Requirements-driven Model-based Testing

In model-based black-box testing of embedded control systems, test suites can
be generated from models with two alternative objectives in mind. (1) The test
suite could aim at uncovering conformance violations; typical conformance
relations are interface language equivalence or refinement. It is assumed that
the model captures the complete expected behaviour of the system under test
(SUT). (2) Alternatively, test suites can be constructed to uncover violations
of specific requirements in an implementation behaviour. To this end, the
requirement has to be specified in addition to the model, using, for example,
temporal logic or test scenario specifications. Another option is to use
modelling languages like SysML SysML17  allowing to relate requirements to
behavioural or structural model elements, making it often unnecessary to add
temporal logic or scenario specifications. Some requirements-driven test
approaches advocate test generation from temporal logic formulas alone
DBLP:conf/issta/WhalenRHM06 , so that a behavioural model becomes unnecessary.
This, however, has the disadvantage that formulas can only refer to interface
variables, making the formulas quite complex to specify. With a behavioural
model at hand, formulas can also refer to internal state variables,
facilitating the expression of requirements DBLP:conf/isola/0001BH18 .

Objective (1) typically applies to protocol testing or any other domain where
the model is sufficiently small to induce conformance test suites of
acceptable size protocoltestsystems95 . Objective (2) applies to domains where
models are too large and too complex to perform conformance tests with
acceptable size and sufficient test strength to uncover conformance
violations. Moreover, development standards for safety-critical control
systems typically require that testing should be requirements-driven, so that
a conformance testing approach that does not relate test cases to requirements
would be inadmissible DO178C ; CENELEC50128 . Finally, requirements-driven
testing is the preferred approach to systematic regression testing: after
changes to the implementation, the requirements affected by these changes are
identified, and it is tested whether the modified SUT conforms to these
requirements. This allows to avoid re-testing the whole test suite, which may
be too time consuming, especially in HW/SW integration testing or system
testing, where test executions need to be performed in physical time and
cannot be sped up by using faster processors or performing them in parallel on
many CPU cores, as is possible for software tests.

###  1.2 Main Contributions

In this article, two novel model-based requirements-driven test strategies are
introduced, and their fault coverage guarantees are proven. Models are
represented as deterministic finite state machines (DFSMs). We are aware of
the fact that FSMs are not well-suited for modelling control systems with
complex and large data types for interfaces and internal state variables. We
have shown, however, that such systems may be abstracted to FSMs after having
calculated state and input equivalence classes on the complex model which is
interpreted, for example, as a Kripke Structure. Test suites with guaranteed
fault coverage calculated for the FSM abstraction give rise to equivalence
class tests with likewise guaranteed fault coverage for the complex system
peleska_sttt_2014 ; Huang2017 . These considerations motivate the study of
testing theories for finite state machines. We restrict ourselves to
deterministic systems, since determinism is always required in the context of
safety-critical control systems.

_Elementary requirements_ are represented as triples $R(q,x,Z)$, where $q$ is
a state in the reference model, $x$ is an input to the DFSM, and $Z$ is a
subset of the machine’s output alphabet, representing the admissible outputs
that may be produced by the SUT after having processed any input sequence
leading the reference model into state $q$. A _composite requirement_ is
specified as a combination of elementary ones. It is easy to see that
implementations whose true behaviour can be represented by a DFSM which is
language-equivalent to that of the reference DFSM automatically fulfil all
specified requirements.

The two strategies have the following characteristics.

  * •

The first strategy is _exhaustive_ in the sense that it provides test suites
that imply requirements satisfaction when passed. When failed, the SUT is
guaranteed to violate language equivalence, but it does not necessarily
violate the composite requirement that is being tested. This approach is
called _exhaustive testing of (composite) requirements_.

  * •

The second strategy is _complete_ in the sense that it provides test suites
that are passed by the SUT if and only if it conforms to the specified
requirement. When a test suite generated according to this strategy is failed,
it is guaranteed that the SUT violates the requirement. On the other hand,
these test suites do not uncover any violations of language conformance, if
these violations are unrelated to the requirement. We call this approach
_complete testing of (composite) requirements_.

Observe that the terms ‘exhaustive’ and ‘complete’ have been adopted from
conformance testing, where a test suite is called ‘sound’ if it is passed by
all conforming implementations, ‘exhaustive’ if non-conforming implementations
will always fail at least one test case, and ‘complete’ if the suite is sound
and exhaustive DBLP:journals/cn/Tretmans96 .

The test suite sizes depend on the requirement and on the difference between
the maximal number $m$ of states assumed for the SUT and the (known) number of
$n$ of states in the minimised reference model. For the first strategy, a
detailed evaluation shows that test effort reductions between 20% and 60% can
be achieved in comparison to test suites generated to prove language
equivalence. We explain why the second strategy is of significant theoretical
value, but usually results in larger test suites and is of lesser practical
value than the first.

The work presented here generalises previous publications
DBLP:conf/pts/Huang017 ; Huang2018 , where requirements referred to outputs of
different criticality only, but could not be linked to states and inputs of
the reference model.

###  1.3 FSM Library

The test suites generated for the evaluation of the test strategies presented
in this article have been calculated using the _fsmlib-cpp_ library, an open
source project programmed in C++. The library contains fundamental algorithms
for processing Mealy Machine FSMs and a variety of model-based test generation
algorithms. Download, contents, and installation of the library is explained
in the lecture notes (PeleskaHuangLectureNotesMBT, , Appendix B) which are
also publicly available.

###  1.4 Overview

In Section 2, basic definitions about finite state machines that are needed
for the elaboration of results are presented. The notion of elementary and
composite requirements is introduced in Section 3. The soundness of the
concept is justified by proving that language equivalence can be alternatively
expressed by composite requirements. In Section 4, we present two DFSM
abstractions that are induced by our requirements notion and needed for the
construction of complete test suites. In Section 5, a pass-relation for
requirements-driven tests and the first main theorem about complete test
suites implying requirements satisfaction are presented. The application of
this main theorem to practical requirements-driven testing is illustrated and
evaluated by means of several experiments in Section 6. In Section 7, the
second main theorem yielding complete test suites to be passed by the SUT if
and only if it fulfils the requirements is introduced and proven. The two test
strategies are compared with respect to their complexity and to their
practical value in Section 8. Section 9 discusses related work, and Section 10
presents a conclusion. In Appendix A, it is explained how the test suites
described in examples throughout the article can be re-generated using the
fsmlib-cpp.

##  2 Basic Definitions

A _finite state machine (FSM)_ is a tuple
$M=(Q,\underline{q},\Sigma_{I},\Sigma_{O},h)$ with finite state space $Q$,
initial state $\underline{q}\in Q$, finite input and output alphabets
$\Sigma_{I},\Sigma_{O}$, and transition relation $h\subseteq
Q\times\Sigma_{I}\times\Sigma_{O}\times Q$. The _specified inputs_ of a state
$q\in Q$ denote the set $in(q)$ of input elements defined by
$in(q)=\\{x\in\Sigma_{I}\leavevmode\nobreak\ |\leavevmode\nobreak\ \exists
y\in\Sigma_{O},q^{\prime}\in Q:(q,x,y,q^{\prime})\in h\\}$.

The _language $L(q)$ of a state $q\in Q$_ is the set of all finite sequences
$\tau=(x_{1},y_{1})\dots(x_{k},y_{k})\in(\Sigma_{I}\times\Sigma_{O})^{*}$ for
which states $q_{1},\dots,q_{k}$ satisfying

$(q,x_{1},y_{1},q_{1})\in h,\dots,(q_{k-1},x_{k},y_{k},q_{k})\in h$ (1)

can be found. The empty sequence $\varepsilon$ is also an element of $L(q)$.
Sequence $\tau$ is called an _I/O-trace_ of $q$, and its length is denoted by
$|\tau|=k$. Sequence $\overline{x}=x_{1}\dots x_{k}$ is called an _input
trace_ , and $\overline{y}=y_{1}\dots y_{k}$ an _output trace_. The _language
$L(M)$ of the FSM $M$_ is the language $L(\underline{q})$ of its initial
state. We also use the alternative notations $\overline{x}/\overline{y}$ for
$\tau$ and $x_{i}/y_{i}$ for $(x_{i},y_{i})$ in $\tau$. Trace segments of some
trace $\tau$ from $p^{th}$ element to $q^{th}$ element are denoted by
$\tau^{[p..q]}$. If $p<q$ as, for example, in $\tau^{[1..0]}$, this denotes
the empty trace $\varepsilon$.

If $L(M)=L(M^{\prime})$, the two machines are called _I/O-equivalent_ or
_language equivalent_ ; if $L(M^{\prime})\subseteq L(M)$, the former is a
_reduction_ of the latter.

An FSM is _deterministic_ , and the machine is called a DFSM, if and only if a
pair $(q,x)\in Q\times\Sigma_{I}$ is associated with at most one transition
element $(q,x,y,q^{\prime})\in h$. The FSM is called _completely specified_ if
and only if every pair $(q,x)\in Q\times\Sigma_{I}$ is associated with at
least one transition element $(q,x,y,q^{\prime})\in h$.

For completely specified DFSMs, every pair $(q,x)\in Q\times\Sigma_{I}$ is
associated with exactly one transition element $(q,x,y,q^{\prime})\in h$. In
this case, the transition relation $h$ can be represented by a _transition
function_ $\delta:Q\times\Sigma_{I}\rightarrow Q$ and an _output function_
$\omega:Q\times\Sigma_{I}\rightarrow\Sigma_{O}$, such that
$(q,x,y,q^{\prime})\in h$ if and only if $(q,x)\in Q\times\Sigma_{I}$ and
$(q,x,y,q^{\prime})=(q,x,\omega(q,x),\delta(q,x))$. Transition functions and
output functions can be extended to sequences of inputs in a natural way by
setting

$\displaystyle\delta$ $\displaystyle:$ $\displaystyle
Q\times\Sigma_{I}^{*}\rightarrow Q$ $\displaystyle\delta(q,\varepsilon)$
$\displaystyle=$ $\displaystyle q$ $\displaystyle\delta(q,x.\overline{x})$
$\displaystyle=$ $\displaystyle\delta(\delta(q,x),\overline{x})$

$\displaystyle\omega$ $\displaystyle:$ $\displaystyle
Q\times\Sigma_{I}^{*}\rightarrow\Sigma_{O}^{*}$
$\displaystyle\omega(q,\varepsilon)$ $\displaystyle=$
$\displaystyle\varepsilon$ $\displaystyle\omega(q,x.\overline{x})$
$\displaystyle=$ $\displaystyle\omega(q,x).\omega(\delta(q,x),\overline{x})$

An FSM is _observable_ if and only if state, input and output uniquely
determine the target state, that is, if the transition relation fulfils

$\forall(q,x,y,q^{\prime}),(q,x,y,q^{\prime\prime})\in
h:q^{\prime}=q^{\prime\prime}.$

DFSMs are automatically observable, and each nondeterministic non-observable
FSM can be transformed to a language-equivalent observable one luo_test_1994 .

The _prime machine_ of a DFSM $M$ is a DFSM $M^{\prime}$ with minimal number
of states, such that $M$ and $M^{\prime}$ have the same language. $M^{\prime}$
is uniquely determined up to isomorphism. The same holds for observable
nondeterministic FSMs Starke72 .

For a DFSM $M$ and a state $q\in Q$, an input trace $\overline{x}$ of an
I/O-trace $\tau\in L(q),\tau=\overline{x}/\overline{y}$, leads to a uniquely
determined target state $q_{k}=\delta(q,\overline{x})$, since there is exactly
one state sequence $q_{1},\dots,q_{k}$ and output trace $\overline{y}$
satisfying (1). We use notation
$q\text{-\text@underline{after}-}\overline{x}=q_{k}$. Note that this is a
partially defined operator, if the DFSM is not completely specified. We extend
its domain with the empty input trace $\varepsilon$ by setting
$q\text{-\text@underline{after}-}\varepsilon=q$. We extend the -after-
operator to set-valued right-hand side operands by setting
$q\text{-\text@underline{after}-}X=\\{q\text{-\text@underline{after}-}\tau\leavevmode\nobreak\
|\leavevmode\nobreak\ \tau\in X\\}$ for $X\subseteq\Sigma^{*}$.

A _state cover_ of a DFSM $M$ is a set $V\subseteq\Sigma_{I}^{*}$ of input
traces such that for each $q\in Q$, there exists a $v\in V$ satisfying
$\underline{q}\text{-\text@underline{after}-}v=q$. In this article, it is
always required that $\varepsilon\in V$, because the empty trace reaches the
initial state, i.e.
$\underline{q}\text{-\text@underline{after}-}\varepsilon=\underline{q}$. The
following well-known lemma shows how a state cover can be constructed in a
very basic (though not optimal) way. It will be used in the proof of the main
theorem.

###### Lemma 1

Let $M=(Q,\underline{q},\Sigma_{I},\Sigma_{O},h)$ be an FSM over input
alphabet $\Sigma_{I}$ and output alphabet $\Sigma_{O}$. Let
$V\subseteq\Sigma_{I}^{*}$ be a finite set of input traces containing the
empty trace $\varepsilon$. Then either

  1. 1.

$\underline{q}\text{-\text@underline{after}-}V$ contains all reachable states,
i.e.,
$\underline{q}\text{-\text@underline{after}-}V=\underline{q}\text{-\text@underline{after}-}\Sigma_{I}^{*}$,
or

  2. 2.

$\underline{q}\text{-\text@underline{after}-}(V\cup V.\Sigma_{I})$ contains at
least one additional state which is not contained in
$\underline{q}\text{-\text@underline{after}-}V$, that is,
$\underline{q}\text{-\text@underline{after}-}V\subsetneq\underline{q}\text{-\text@underline{after}-}(V\cup
V.\Sigma_{I})$.

###### Proof

See, for example, (PeleskaHuangLectureNotesMBT, , Lemma 4.2). ∎

##  3 Requirements

###  3.1 Requirements and Acceptable Deviations – Motivation

In this section, elementary requirements are introduced as assertions stating
that specific transitions of the reference model need to be performed
correctly, whenever the SUT resides in a state corresponding to the
transition’s source state in the reference model. While, just as in the case
of conformance testing, the correct behaviour is specified by the reference
model, an _acceptable deviation_ is also specified for each requirement. Such
a deviation consists of a set of outputs that are considered as “harmless” for
the specified state and input pair, though the correct output specified in the
reference model is still the preferred result.

###### Example 1

Consider a speed monitor in a train that automatically triggers the service
brakes when the train exceeds the admissible velocity. If the emergency brakes
are triggered instead of the service brakes, this would be considered as an
acceptable deviation: the safety goal to slow down the train will be reached
even better than with the service brakes. Only the passenger comfort is
reduced, since the emergency brakes are much harder than the normal ones. On
the other hand, if the brakes are released instead of triggering them, this
would lead to a safety violation and therefore be an unacceptable deviation.∎

The reason to introduce acceptable deviations is that the test effort can be
reduced in a considerable way if (a) only critical requirements are tested
with complete strategies, instead of using a complete conformance suite, and
(b) we abstain from insisting on the exact behaviour specified in the
reference model, as long as the resulting deviations are still acceptable.

###  3.2 Elementary Requirements, Acceptable Deviations, and Satisfaction

Formalising this intuitive concept, let
$M=(Q,\underline{q},\Sigma_{I},\Sigma_{O},h)$ be a reference model,
represented by a deterministic, completely specified prime FSM with $|Q|=n\geq
2$. Let $\omega_{M}:Q\times\Sigma_{I}\rightarrow\Sigma_{O}$ denote the output
function of $M$. An _elementary requirement_ is denoted by $R(q,x,Z)$, where

  1. 1.

$q\in Q$,

  2. 2.

$x\in\Sigma_{I}$, and

  3. 3.

$Z\subset\Sigma_{O}$, such that $Z\neq\Sigma_{O}$ and $\omega_{M}(q,x)\in Z$.

Output $\omega_{M}(q,x)$ is called the _expected output_ , and the outputs
$y\in Z-\\{\omega_{M}(q,x)\\}$ are called _acceptable deviations_. The set $Z$
is required to be a true subset of the output alphabet, because it would not
make sense to specify a requirement where any output $y\in\Sigma_{O}$ is
considered as acceptable.

An elementary requirement $R(q,x,Z)$ is _fulfilled with acceptable deviations_
(written $S\models R(q,x,Z)$) by some SUT
$S=(S,\underline{s},\Sigma_{I},\Sigma_{O},h_{s})$, if, after any input trace
$\overline{x}\in\Sigma_{I}^{*}$ leading to $q$ in the reference model, the
input $x$ given to $S$ results in an output $z\in Z$. To formalise this
notion, define

$\Pi(q)=\\{\overline{x}\in\Sigma_{I}^{*}\leavevmode\nobreak\
|\leavevmode\nobreak\
\underline{q}\text{-\text@underline{after}-}\overline{x}=q\\};$

this is the (possibly infinite) set of all input traces reaching $q$ in
reference model $M$, when starting from the initial state $\underline{q}$.
Then specify

$S\models R(q,x,Z)\ \text{if and only if}\
\forall\pi\in\Pi(q):\omega_{S}(\underline{s}\text{-\text@underline{after}-}\pi,x)\in
Z.$ (2)

###  3.3 Composite Requirements for DFSMs

A _composite requirement $R$_ is written as a conjunction

$R\equiv R(q_{1},x_{1},Z_{1})\wedge\dots\wedge R(q_{k},x_{k},Z_{k})$

of elementary requirements and interpreted in the natural way as

$S\models R\ \text{if and only if}\ (S\models
R(q_{1},x_{1},Z_{1}))\wedge\dots\wedge(S\models R(q_{k},x_{k},Z_{k})).$

This means that the SUT $S$ fulfils each of the elementary requirements
involved.

###### Example 2

As a running example, we will consider a reference model represented by the
state machine $M$ shown in Fig. 1. The initial state $q_{0}$ is marked by a
double circle. On $M$, we specify the composite requirement

$R\equiv R(q_{0},a,\\{0,1\\})\wedge R(q_{1},b,\\{0,2\\})\wedge
R(q_{2},a,\\{0,1\\}).$

Consider an implementation with behaviour as modelled by the DFSM $S$ in Fig.
2. The implementation is not language equivalent to $M$: for example,
$\omega_{M}(q_{0},a.a.a)=1.0.0$, but $\omega_{S}(s_{0},a.a.a)=1.0.1$. However,
the following example traces show that $S$ might still fulfil $R$ with
acceptable deviation111This will be established more formally in the
consecutive sections, where a complete test strategy for checking the
implementation’s compliance to composite requirements is elaborated.: (a) For
sample input trace $b.b\in\Pi(q_{0})$, we observe that
$\omega_{S}(s_{0}\text{-\text@underline{after}-}b.b,a)=\omega_{S}(s_{0},a)=1=\omega_{M}(q_{0},a)=\omega_{M}(q_{0}\text{-\text@underline{after}-}b.b,a)$,
so this result conforms to $R(q_{0},a,\\{0,1\\})$ without any deviation. (b)
For $a.b\in\Pi(q_{1})$, we get
$\omega_{S}(s_{0}\text{-\text@underline{after}-}a.b,b)=\omega_{S}(s_{1},b)=0=\omega_{M}(q_{1},b)=\omega_{M}(q_{0}\text{-\text@underline{after}-}a.b,b)$,
so this result also conforms to the applicable elementary requirement
$R(q_{1},b,\\{0,2\\})$ without any deviation. (c) For $a.a\in\Pi(q_{2})$,
$\omega_{S}(s_{0}\text{-\text@underline{after}-}a.a,a)=\omega_{S}(s_{0},a)=1$,
whereas
$\omega_{M}(q_{0}\text{-\text@underline{after}-}a.a,a)=\omega_{M}(q_{2},a)=0$.
But this deviation is still acceptable, since the applicable elementary
requirement $R(q_{2},a,\\{0,1\\})$ accepts both outputs $0$ and $1$. ∎

Figure 1: Reference model $M$.

Figure 2: Implementation model $S$.

###  3.4 Characterisation of Language Equivalence by Composite Requirements.

A “very large” composite requirement can be defined by stating that the SUT
should conform to every transition of the reference model, without leaving any
alternatives for the expected output. The following theorem states that this
requirement exactly captures language equivalence.

###### Theorem 3.1

Let $M=(Q,\underline{q},\Sigma_{I},\Sigma_{O},h_{M})$ and
$S=(S,\underline{s},\Sigma_{I},\Sigma_{O},h_{S})$ be deterministic, completely
specified prime machines over the same alphabet with output functions
$\omega_{M}:Q\times\Sigma_{I}\rightarrow{\Sigma_{O}}$ and
$\omega_{S}:Q\times\Sigma_{I}\rightarrow{\Sigma_{O}}$, respectively. Define
composite requirement

$R_{eq}=\bigwedge_{(q,x)\in Q\times\Sigma_{I}}R(q,x,\\{\omega_{M}(q,x)\\}).$

Then

$L(S)=L(M)\quad\text{if and only if}\quad S\models R_{eq}.$

###### Proof

It is obvious that $L(S)=L(M)$ implies $S\models R_{eq}$, since $M\models
R_{eq}$ by construction of $R_{eq}$. Therefore, we only need to show that
$S\models R_{eq}$ implies $L(S)=L(M)$. Suppose $L(S)\neq L(M)$. Then there
exists a shortest input sequence $\overline{x}\in\Sigma_{I}^{*}$ such that
$\omega_{S}(\underline{s},\overline{x})\neq\omega_{M}(\underline{q},\overline{x})$,
where $\omega_{S},\omega_{M}$ are the natural extension of the output
functions to input sequences introduced in Section 2. Since $\varepsilon\in
L(M)\cap L(S)$, $|\overline{x}|\geq 1$ and $\overline{x}$ can be written as
$\overline{x}=\pi.x$, for some $\pi\in\Sigma_{I}^{*}$ and $x\in\Sigma_{I}$.
Then we have
$\omega_{S}(\underline{s},\pi)=\omega_{M}(\underline{q},\pi)\wedge\omega_{S}(\underline{s}\text{-\text@underline{after}-}\pi,x)\neq\omega_{M}(\underline{q}\text{-\text@underline{after}-}\pi,x)$.
Hence $S\not\models
R(\underline{q}\text{-\text@underline{after}-}\pi,x,\\{\omega_{M}(\underline{q}\text{-\text@underline{after}-}\pi,x)\\})$,
and this elementary requirement is a conjunct of the composite requirement
$R_{eq}$. Therefore, $S\not\models R_{eq}$ follows. ∎

##  4 Requirements-driven DFSM Abstraction

Given a reference model $M$ and associated elementary requirements
$R(q_{i},x_{i},Z_{i})$ with $i=1,\dots,k$ as introduced above, we will now
introduce two abstractions $M\rightarrow M_{1}\rightarrow M_{2}$ that are
needed to create test suites allowing to verify that an SUT $S$ fulfils all
$R(q_{i},x_{i},Z_{i})$ without having to test for the stronger property
language equivalence.

  1. 1.

$M_{1}$ abstracts from concrete $M$-outputs by using sets of output events
$Z_{i}\subset\Sigma_{O}$ where requirement $R(q_{i},x_{i},Z_{i})$ is involved,
and using the whole output alphabet $\Sigma_{O}$ as don’t care symbol to
specify outputs unrelated to any requirement.

  2. 2.

$M_{2}$ is the prime machine of $M_{1}$. Note that $M_{1}$ may be no longer
minimal, since some $M$-states may not be distinguishable anymore due to
output abstraction.

###  4.1 Construction of $M_{1}$

Let $*=\Sigma_{O}$ denote the _don’t care symbol_ specifying that “any output
is allowed” in certain situations. Define
$\Sigma_{O}^{\prime}=\\{*,Z_{1},\dots,Z_{k}\\}$ as the new output alphabet of
a completely specified, deterministic abstraction $M_{1}$ with state space
$Q$, initial state $\underline{q}$, input alphabet $\Sigma_{I}$, and output
and transition functions specified as follows.

  1. 1.

The transition function $\delta_{M_{1}}$ of $M_{1}$ coincides with that of
$M$, that is, $\delta_{M_{1}}=\delta_{M}$.

  2. 2.

The output function $\omega_{M_{1}}$ of $M_{1}$ is defined by

$\displaystyle\omega_{M_{1}}(q_{i},x_{i})$ $\displaystyle=Z_{i}$
$\displaystyle\ \text{for}\ i\in\\{1,\dots,k\\}$ (3)
$\displaystyle\omega_{M_{1}}(q,x)$ $\displaystyle=*$ $\displaystyle\
\text{for}\ (q,x)\in
Q\times\Sigma_{I}\setminus\\{(q_{1},x_{1}),\dots,(q_{k},x_{k})\\}$ (4)

By construction, $M_{1}$ abstracts all outputs related to elementary
requirements $R(q_{i},x_{i},Z_{i})$ to $Z_{i}$ and all outputs that are
unrelated to any requirement to $*$. Being unrelated to any requirement means
that the (state,input)-pair $(q,x)$ occurring in the original transition
$(q,x,y,q^{\prime})\in h$ differs from all $(q_{i},x_{i})$ used in the
specification of some requirement $R(q_{i},x_{i},Z_{i})$.

###  4.2 Construction of $M_{2}$

Let $M_{2}$ be the prime machine of $M_{1}$. If $\\{q_{1},\dots,q_{k}\\}=Q$
and $(x_{i},Z_{i})=(x_{j},Z_{j})$, for all $i,j=1,\dots,k$, then $M_{2}$
contains only one state, otherwise, $M_{2}$ contains at least two states.
Denote the states in $M_{2}$ by $[q]$, which is the equivalence class of state
$q$ in $M_{1}$ :

$[q]=\\{q^{\prime}\in Q\leavevmode\nobreak\ |\leavevmode\nobreak\
L_{M_{1}}(q^{\prime})=L_{M_{1}}(q)\\}$

The transition relation of $M_{2}$ is denoted by
$h_{2}=\\{([q],x,y,[q^{\prime}])\leavevmode\nobreak\ |\leavevmode\nobreak\
(q,x,y,q^{\prime})\in h_{1}\\}$. We have
$[q\text{-\text@underline{after}-}\overline{x}]=[q]\text{-\text@underline{after}-}\overline{x}$,
for any $q\in Q$ and $\overline{x}\in\Sigma_{I}^{*}$, where the transition
”-after-” from the left side is according to $h$ and $h_{1}$, since $M_{1}$
contains the same transitions of $M$ up to the outputs. The ”-after-” from the
right side is according to $h_{2}$.

Let $n^{\prime}=|Q^{\prime}|\geq 1$. For any
$q_{i},q_{j}\in\\{q_{1},\dots,q_{k}\\}$, $[q_{i}]=[q_{j}]$ implies
$x_{i}/Z_{i}=x_{j}/Z_{j}$. Let $q\in Q$ and suppose $[q]=[q_{i}]$ for some
$i=1,\dots,k$. Then
$(q,x_{i},Z_{i})\in\\{(q_{1},x_{1},Z_{1}),\dots,(q_{k},x_{k},Z_{k})\\}$,
because otherwise the output of $(q,x_{i})$ in $h_{1}$ is $*$ and $*\neq
Z_{i}$, contradicting the fact that $q$ and $q_{i}$ are equivalent. Hence,
from $[q]=[q_{i}]$ follows $q=q_{j}$ for some $j=1,\dots,k$. Define

$[\Pi(q_{i})]=\bigcup_{j\in\\{\ell\in\\{1,\dots,k\\}\leavevmode\nobreak\
|\leavevmode\nobreak\ [q_{\ell}]=[q_{i}]\\}}\Pi(q_{j}).$

This is the set of all input traces leading to states $q_{j}$ in $M$ that are
equivalent to $q_{i}$ in $M_{1}$.

###### Example 3

For the reference model $M$ introduced in Example 2 and the composite
requirement $R$ specified there, the abstracted machine $M_{1}$ is depicted in
Fig. 3. Its minimised machine $M_{2}$ is shown in Fig. 4. ∎

Figure 3: Abstraction $M_{1}$ of reference model $M$ from Example 2.

Figure 4: Minimised version of $M_{1}$.

##  5 Exhaustive Testing of Composite Requirements

###  5.1 Test Cases, Test Suites, and Pass Criteria

A _test suite_ TS is a set of input traces $\overline{x}\in\Sigma_{I}$; the
latter are called _test cases_. The _expected result_ associated with test
case $\overline{x}$ is the output trace
$\omega_{M}(\underline{q},\overline{x})$ calculated from the reference model.
An implementation $S=(S,\underline{s},\Sigma_{I},\Sigma_{O},h_{S})$ _passes_
test case $\overline{x}$, if and only if the associated outputs observed when
running $\overline{x}$ against $S$ conform to the expected results. More
formally,

$S\ \underline{\text{\bf pass}}_{\Rightarrow}\ \overline{x}\ \ \text{if and
only if}\ \
\omega_{S}(\underline{s},\overline{x})=\omega_{M}(\underline{q},\overline{x}).$

Implementation $S$ _passes the test suite TS_ if and only if $S$ passes all
test cases, that is,

$S\ \underline{\text{\bf pass}}_{\Rightarrow}\ \text{TS}\ \ \text{if and only
if}\ \ \forall\overline{x}:\text{TS}:S\ \underline{\text{\bf
pass}}_{\Rightarrow}\overline{x}.$

We say that a test suite TS is _exhaustive with respect to composite
requirement $R=R(q_{1},x_{1},Z_{1})\wedge\dots\wedge R(q_{k},x_{k},Z_{k})$_ if
and only if

$S\ \underline{\text{\bf pass}}_{\Rightarrow}\ \text{TS}\Rightarrow S\models
R.$ (5)

In the remainder of this section, we will construct a finite test suite
$\text{TS}_{\Rightarrow}$, whose size depends on the reference model $M$, the
(composite) requirement, and the assumed maximal number $m$ of states in the
implementation DFSM $S$. We will show that $\text{TS}_{\Rightarrow}$ is
exhaustive with respect to composite requirement
$R=R(q_{1},x_{1},Z_{1})\wedge\dots\wedge R(q_{k},x_{k},Z_{k})$ for the fault
domain of completely specified, deterministic FSMs with at most $m$ states.

Obviously, if $S$ is I/O-equivalent to $M$, then $S$ satisfies the composite
requirement $R$. Hence, any SUT $S$, with $S\not\models R$ will fail any
complete test suite for fault model $F=(M,\sim,D)$, where $S\in D$ and $\sim$
is the language equivalence conformance relation. Therefore, any complete test
suite for fault model $F=(M,\sim,D)$ with $S\in D$ satisfies the above two
conditions. Our objective is to introduce a test strategy leading to fewer
test cases than the well-known strategies for generating test suites checking
language equivalence.

It should be emphasised that the expected results associated with each test
case reject any deviation of the SUT from the outputs expected according to
the reference model. Therefore, if $S$ is in a state corresponding to some
state $q_{i}$ in $M$ and reacts to input $x_{i}$ with some output $y$ which is
in $Z_{i}$ but which differs from the expected value $\omega_{M}(q,x_{i})$,
the test execution will fail. It will be illustrated below, however, that the
introduction of admissible deviation $y\in Z_{i}-\\{\omega_{M}(q,x_{i})\\}$
may lead to fewer test cases. This reduction comes at the cost that some
violations of expected results may be overlooked; but it can still be
guaranteed that these violations are always admissible deviations. For
transitions that are not linked to any elementary requirement
$R(q_{i},x_{i},Z_{i})$, no guarantees are made whatsoever.

Moreover, note that according to condition (5), failing the test suite does
not necessarily imply that $R$ is violated: the test suite may also fail
because an erroneous output is uncovered which is unrelated to any elementary
requirement in $R$. This conforms to our understanding of a “reasonably
designed” test oracle. Any detected deviation in comparison to the reference
model will lead to the test case to fail; it is just not guaranteed that all
errors that are unrelated to $R$ will be uncovered.

###  5.2 Test Suite Construction

Let $V$, $\varepsilon\in V$, be a state cover of $M$. We define three
auxiliary sets $A,B,C$ containing pairs of input traces.

$\displaystyle A$ $\displaystyle=V\times V$ (6) $\displaystyle B$
$\displaystyle=V\times V.\bigcup_{i=1}^{m-n+1}\Sigma_{I}^{i}$ (7)
$\displaystyle C$ $\displaystyle=\\{(\alpha,\beta)\leavevmode\nobreak\
|\leavevmode\nobreak\ \alpha\in\text{pref}(\beta),\alpha,\beta\in
V.\bigcup_{i=1}^{m-n+1}\Sigma_{I}^{i}\\}$ (8)

For any $\alpha,\beta\in A\cup B\cup C$, define

$\displaystyle\Delta_{M}(\alpha,\beta)$
$\displaystyle=\\{\gamma\in\Sigma_{I}^{*}\leavevmode\nobreak\
|\leavevmode\nobreak\
\omega_{M}(\underline{q}\text{-\text@underline{after}-}\alpha,\gamma)\neq\omega_{M}(\underline{q}\text{-\text@underline{after}-}\beta,\gamma)\\}$
(9) $\displaystyle\Delta_{M_{1}}(\alpha,\beta)$
$\displaystyle=\\{\gamma\in\Sigma_{I}^{*}\leavevmode\nobreak\
|\leavevmode\nobreak\
\omega_{M_{1}}(\underline{q}\text{-\text@underline{after}-}\alpha,\gamma)\neq\omega_{M_{1}}(\underline{q}\text{-\text@underline{after}-}\beta,\gamma)\\}$
(10)

The set $\Delta_{M}(\alpha,\beta)$ contains all input traces distinguishing
the states $q\text{-\text@underline{after}-}\alpha$ and
$q\text{-\text@underline{after}-}\beta$ in $M$ by yielding different output
traces when applied to these states. Set $\Delta_{M_{1}}(\alpha,\beta)$
contains all input traces distinguishing the states
$q\text{-\text@underline{after}-}\alpha$ and
$q\text{-\text@underline{after}-}\beta$ in $M_{1}$. Note that
$\Delta_{M}(\alpha,\beta)$ and $\Delta_{M_{1}}(\alpha,\beta)$ may be empty,
since $\underline{q}\text{-\text@underline{after}-}\alpha$ and
$\underline{q}\text{-\text@underline{after}-}\beta$ are not necessarily
distinguishable in $M$ or $M_{1}$, respectively. For an arbitrary set
$P\subseteq\Sigma_{I}^{*}\times\Sigma_{I}^{*}$ of pairs of input traces,
define $P(M)\subseteq P$ and $P(M_{1})\subseteq P$ by

$\displaystyle(\alpha,\beta)\in P(M)$
$\displaystyle\Leftrightarrow(\alpha,\beta)\in
P\wedge\Delta_{M}(\alpha,\beta)\neq\varnothing$ (12)
$\displaystyle(\alpha,\beta)\in P(M_{1})$
$\displaystyle\Leftrightarrow(\alpha,\beta)\in
P\wedge\Delta_{M_{1}}(\alpha,\beta)\neq\varnothing$ (13)

We will apply this notation to the sets $A,B,C$ defined above: $A(M)$, for
example, is the subset of all trace pairs $(\alpha,\beta)$ from $A$ whose
target states $\underline{q}\text{-\text@underline{after}-}\alpha$ and
$\underline{q}\text{-\text@underline{after}-}\beta$, respectively, are
distinguishable in $M$.

###  5.3 Main Theorem on Exhaustive Test Suites

The following main theorem shows that the criteria (14) and (15) suffice to
guarantee that the test suite $\text{TS}_{\Rightarrow}$ is exhaustive.

###### Theorem 5.1

Let $m\geq n$ be a positive integer. Let
$S=(S,\underline{s},\Sigma_{I},\Sigma_{O},h_{s})$ be a minimal DFSM with
$|S|\leq m$. Let $\text{TS}_{\Rightarrow}\subseteq\Sigma_{I}^{*}$ be any test
suite satisfying

$\displaystyle
V.\bigcup_{i=0}^{m-n+1}\Sigma_{I}^{i}\subseteq\text{TS}_{\Rightarrow},\,\text{and}$
(14) $\displaystyle\forall(\alpha,\beta)\in A(M)\cup B(M_{1})\cup
C(M_{1}):\exists\gamma\in\Delta_{M}(\alpha,\beta):\alpha.\gamma,\beta.\gamma\in\text{TS}_{\Rightarrow}$
(15)

Then $\text{TS}_{\Rightarrow}$ is exhaustive for composite requirement
$R=R(q_{1},x_{1},Z_{1})\wedge\dots\wedge R(q_{k},x_{k},Z_{k})$, that is,

$S\ \underline{\text{\bf pass}}_{\Rightarrow}\
\text{TS}_{\Rightarrow}\Rightarrow S\models R.$

###### Proof

Suppose $S\ \underline{\text{\bf pass}}_{\Rightarrow}\
\text{TS}_{\Rightarrow}$. We first show that
$V.\bigcup_{i=0}^{m-n}\Sigma_{I}^{i}$ is a state cover of $S$. Since $V$ is a
state cover of $M$ and $M$ is a prime machine, there are input traces
$\alpha.\gamma,\beta.\gamma$ in $\text{TS}_{\Rightarrow}$ for each pair of the
$n$ states in $Q$, such that $\alpha,\beta\in V$ and states
$\underline{q}\text{-\text@underline{after}-}\alpha$ and
$\underline{q}\text{-\text@underline{after}-}\beta$ are distinguished by
$\gamma$ in $M$. Since $S$ passes these test cases, this also distinguishes
$n$ states in $S$. Since $S$ has at most $m$ states, Lemma 1 can be applied to
conclude that $V.\bigcup_{i=0}^{m-n}\Sigma_{I}^{i}$ reaches all states of $S$.

Suppose $S\,\not\models\,R$. Then there is some $t\in\\{1,\dots,k\\}$ with
$S\not\models R(q_{t},x_{t},Z_{t})$. Hence there exists $\pi\in\Pi(q_{t})$
with $\omega_{M}(\underline{q}\text{-\text@underline{after}-}\pi,x_{t})\in
Z_{t}$, but
$\omega_{S}(\underline{q}\text{-\text@underline{after}-}\pi,x_{t})\not\in
Z_{t}$. Lifting these observations to the abstraction $M_{2}$ introduced in
Section 4.2, this induces the existence of input traces
$\pi_{2}\in[\Pi(q_{t})]$ such that
$\omega_{M_{2}}([\underline{q}]\text{-\text@underline{after}-}\pi_{2},x_{t})=Z_{t}$
and
$\omega_{S}(\underline{s}\text{-\text@underline{after}-}\pi_{2},x_{t})\not\in
Z_{t}$. Since $\varepsilon\in V$, each $\pi_{2}\in[\Pi(q_{t})]$ can be
structured as $\pi_{2}=v.\tau$ with $v\in V$ and $\tau\in\Sigma_{I}^{*}$. Let
$\tau$ be a shortest sequence such that

$\exists v\in
V:v.\tau\in[\Pi(q_{t})]\wedge\omega_{S}(\underline{s}\text{-\text@underline{after}-}v.\tau,x_{t})\not\in
Z_{t}.$ (16)

Since $S\ \underline{\text{\bf pass}}_{\Rightarrow}\ \text{TS}_{\Rightarrow}$
and $V.\bigcup_{i=0}^{m-n+1}\Sigma_{I}^{i}\subseteq\text{TS}_{\Rightarrow}$,
we have $|\tau|\geq m-n+1$, because otherwise, the input trace $v.\tau.x_{t}$
would have been tested, and the test suite would have failed.

Let $\tau_{i}=\tau^{[1..i]},i\leq m-n+1$. Then $v.\tau_{i}\neq v.\tau_{j}$ for
all $i\neq j$. Let $V=\\{v_{1},\dots,v_{n}\\}$. Then $v_{i}\neq v_{j}$ for
$i\neq j$, since $V$ reaches $n$ different states in $M$. Suppose
$v_{i}=v.\tau_{j}$ for some $i,j$. Let $\iota$ be the suffix of $\tau_{j}$
with $\tau_{j}.\iota=\tau$. Then
$v_{i}.\iota=v.\tau_{j}.\iota=v.\tau\in[\Pi(q_{t})]$, and $|\iota|<|\tau|$, a
contradiction to the assumption that $\tau\in\Sigma_{I}^{*}$ is a shortest
sequence satisfying condition (16). As a consequence, the set
$U=\\{v_{1},\dots,v_{n},v.\tau_{1},\dots,v.\tau_{m-n+1}\\}$ contains $m+1$
elements. Observe that $U\subseteq\text{TS}_{\Rightarrow}$, since all elements
start with a $v\in V$ and – if extended by some $\tau_{i}$ – are followed by
an input trace of length less or equal to $m-n+1$.

Since $S$ contains only $m$ states, there exist $\alpha\neq\beta\in U$
reaching the same state in $S$, that is,
$\underline{s}\text{-\text@underline{after}-}\alpha=\underline{s}\text{-\text@underline{after}-}\beta$.
Assume that
$\underline{q}\text{-\text@underline{after}-}\alpha,\underline{q}\text{-\text@underline{after}-}\beta$
are not equivalent in $M_{1}$. This would imply $\\{\alpha,\beta\\}\subseteq
A(M)\cup B(M_{1})\cup C(M_{1})$ and the existence of a distinguishing trace
$\gamma\in\Delta_{M}(\alpha,\beta)$ such that
$\\{\alpha.\gamma,\beta.\gamma\\}\subseteq\text{TS}_{\Rightarrow}$ (see (15)).
This would lead to a failed test execution, since $\gamma$ cannot distinguish
$\underline{s}\text{-\text@underline{after}-}\alpha=\underline{s}\text{-\text@underline{after}-}\beta$,
but would lead to different outputs when applied to
$\underline{q}\text{-\text@underline{after}-}\alpha$ and
$\underline{q}\text{-\text@underline{after}-}\beta$. This contradiction
implies that
$\underline{q}\text{-\text@underline{after}-}\alpha,\underline{q}\text{-\text@underline{after}-}\beta$
are equivalent in $M_{1}$. As a consequence, $\\{\alpha,\beta\\}$ cannot be
contained in $V$, since pairs from $V$ always reach distinguishable states in
$M$. Without loss of generality, we therefore assume that one of the cases (a)
$\alpha=v_{i}\in V,\beta=v.\tau_{j}$, or (b)
$\alpha=v.\tau_{i},\beta=v.\tau_{j},i<j$ applies.

Let $\iota$ be the suffix of $\tau_{j}$ with $\tau_{j}.\iota=\tau$ (in the
case $j=m-n+1=|\tau|,\iota=\varepsilon$). Then $\beta.\iota=v.\tau$. Since
$\underline{q}\text{-\text@underline{after}-}\alpha,\underline{q}\text{-\text@underline{after}-}\beta$
are equivalent states in $M_{1}$, we obtain that
<EMAIL_ADDRESS>and
<EMAIL_ADDRESS>are equivalent
states in $M_{1}$, hence $\alpha.\iota\in[\Pi(q_{t})]$. Since
$\underline{s}\text{-\text@underline{after}-}\beta=\underline{s}\text{-\text@underline{after}-}\alpha$
in $S$, we conclude that
$\underline{s}\text{-\text<EMAIL_ADDRESS>and
$\omega_{S}(\underline{s}\text{-\text@underline{after}-}\beta.\iota,x_{t})=\omega_{S}(\underline{s}\text{-\text@underline{after}-}\alpha.\iota,x_{t})\not\in
Z_{t}$. In the case $\alpha=v_{i}\in V$, we have $|\iota|<|\tau|$. For
$\alpha=v.\tau_{i}$, we have $\alpha.\iota=v.\tau_{i}.\iota$ and
$|\tau_{i}.\iota|<|\tau|$. Both cases contradict the assumption that
$\tau\in\Sigma_{I}^{*}$ is a shortest sequence satisfying condition (16). This
contradiction implies that $S\ \underline{\text{\bf pass}}_{\Rightarrow}\
\text{TS}_{\Rightarrow}$ and $S\not\models R$ cannot both be true and
completes the proof of the theorem. ∎

Algorithms for creating test suites according to formulas (14) and (15) have
been described in the original work DBLP:conf/forte/DorofeevaEY05  and in
Huang2018 .

###### Example 4

Consider again reference model $M$ and the (in black box testing practise
unknown) implementation model $S$ from Example 2. $M$ is minimal and has $n=3$
states. Under the hypothesis that the minimised model of the true
implementation behaviour also has $m=3$ states, the following test suite with
4 test cases has been calculated according to the rules (14) and (15).

$a.a.b,a.b.b,b.a.b,b.b.a$

Applying this test suite to the implementation model $S$ results in I/O-traces

$a.a.b/1.0.2,a.b.b/1.2.0,b.a.b/2.0.0,b.b.a/2.0.1$

These executions conform to the reference model $M$, so the implementation
passes the suite. This shows that $S\models R$ holds.

Applying the complete H-method to $M$ and hypothesis $m=n=3$ results in 5 test
cases. These comprise the ones calculated according to (14) and (15), adding a
fifth test case $a.a.a$. This new test case reveals the fact that $S$ is not
language equivalent to $M$, since $S$ produces $a.a.a/1.0.1$ where
$a.a.a/1.0.0$ had been expected according to reference model $M$.

In Appendix A, it is explained how these test suites can be automatically
generated using the library fsmlib-cpp mentioned in the introduction. ∎

##  6 Evaluation Using a Real-World Example

###  6.1 Fasten Seatbelt and Return-to-Seat Sign Control

The following experiment is a (slightly simplified) real-world example
concerning safety-related and uncritical indications in an aircraft
cabin222The application used in this experiment has been originally published
in (Huang2018, , Section 4.1). The application description has been reproduced
here in its original form, in order to make this article sufficiently self-
contained..

Table 1: State-transition table of DFSM specifying the control of FSB signs
and RTS signs in an aircraft cabin.

| f0 | f1 | f2 | d1 | d0 | e1 | e0 | a1 | a0
---|---|---|---|---|---|---|---|---|---
$\mathbf{s_{0}}$ |  $s_{0}$/00 |  $s_{1}$/11 |  $s_{2}$/00 |  $s_{3}$/10 |  $s_{0}$/00 |  $s_{6}$/10 |  $s_{0}$/00 |  $s_{12}$/00 |  $s_{0}$/00
$\mathbf{s_{1}}$ |  $s_{0}$/00 |  $s_{1}$/11 |  $s_{2}$/00 |  $s_{4}$/10 |  $s_{1}$/11 |  $s_{7}$/10 |  $s_{1}$/11 |  $s_{13}$/11 |  $s_{1}$/11
$\mathbf{s_{2}}$ |  $s_{0}$/00 |  $s_{1}$/11 |  $s_{2}$/00 |  $s_{5}$/10 |  $s_{2}$/00 |  $s_{8}$/10 |  $s_{2}$/00 |  $s_{14}$/11 |  $s_{2}$/00
$\mathbf{s_{3}}$ |  $s_{3}$/10 |  $s_{4}$/10 |  $s_{5}$/10 |  $s_{3}$/10 |  $s_{0}$/00 |  $s_{9}$/10 |  $s_{3}$/10 |  $s_{15}$/10 |  $s_{3}$/10
$\mathbf{s_{4}}$ |  $s_{3}$/10 |  $s_{4}$/10 |  $s_{5}$/10 |  $s_{4}$/10 |  $s_{1}$/11 |  $s_{11}$/10 |  $s_{4}$/10 |  $s_{16}$/10 |  $s_{4}$/10
$\mathbf{s_{5}}$ |  $s_{3}$/10 |  $s_{4}$/10 |  $s_{5}$/10 |  $s_{5}$/10 |  $s_{2}$/00 |  $s_{11}$/10 |  $s_{5}$/10 |  $s_{17}$/10 |  $s_{5}$/10
$\mathbf{s_{6}}$ |  $s_{6}$/10 |  $s_{7}$/10 |  $s_{8}$/10 |  $s_{9}$/10 |  $s_{6}$/10 |  $s_{6}$/10 |  $s_{0}$/00 |  $s_{18}$/10 |  $s_{6}$/10
$\mathbf{s_{7}}$ |  $s_{6}$/10 |  $s_{7}$/10 |  $s_{8}$/10 |  $s_{10}$/10 |  $s_{7}$/10 |  $s_{7}$/10 |  $s_{1}$/11 |  $s_{19}$/10 |  $s_{7}$/10
$\mathbf{s_{8}}$ |  $s_{6}$/10 |  $s_{7}$/10 |  $s_{8}$/10 |  $s_{11}$/10 |  $s_{8}$/10 |  $s_{8}$/10 |  $s_{2}$/00 |  $s_{20}$/10 |  $s_{8}$/10
$\mathbf{s_{9}}$ |  $s_{9}$/10 |  $s_{10}$/10 |  $s_{11}$/10 |  $s_{9}$/10 |  $s_{6}$/10 |  $s_{9}$/10 |  $s_{3}$/10 |  $s_{21}$/10 |  $s_{9}$/10
$\mathbf{s_{10}}$ |  $s_{9}$/10 |  $s_{10}$/10 |  $s_{11}$/10 |  $s_{10}$/10 |  $s_{7}$/10 |  $s_{10}$/10 |  $s_{4}$/10 |  $s_{22}$/10 |  $s_{10}$/10
$\mathbf{s_{11}}$ |  $s_{9}$/10 |  $s_{10}$/10 |  $s_{11}$/10 |  $s_{11}$/10 |  $s_{8}$/10 |  $s_{11}$/10 |  $s_{5}$/10 |  $s_{23}$/10 |  $s_{11}$/10
$\mathbf{s_{12}}$ |  $s_{12}$/00 |  $s_{13}$/11 |  $s_{14}$/11 |  $s_{15}$/10 |  $s_{12}$/00 |  $s_{18}$/10 |  $s_{12}$/00 |  $s_{12}$/00 |  $s_{0}$/00
$\mathbf{s_{13}}$ |  $s_{12}$/00 |  $s_{13}$/11 |  $s_{14}$/11 |  $s_{16}$/10 |  $s_{13}$/11 |  $s_{19}$/10 |  $s_{13}$/11 |  $s_{13}$/11 |  $s_{1}$/11
$\mathbf{s_{14}}$ |  $s_{12}$/00 |  $s_{13}$/11 |  $s_{14}$/11 |  $s_{17}$/10 |  $s_{14}$/11 |  $s_{20}$/10 |  $s_{14}$/11 |  $s_{14}$/11 |  $s_{2}$/00
$\mathbf{s_{15}}$ |  $s_{15}$/10 |  $s_{16}$/10 |  $s_{17}$/10 |  $s_{15}$/10 |  $s_{12}$/00 |  $s_{21}$/10 |  $s_{15}$/10 |  $s_{15}$/10 |  $s_{3}$/10
$\mathbf{s_{16}}$ |  $s_{15}$/10 |  $s_{16}$/10 |  $s_{17}$/10 |  $s_{16}$/10 |  $s_{13}$/11 |  $s_{22}$/10 |  $s_{16}$/10 |  $s_{16}$/10 |  $s_{4}$/10
$\mathbf{s_{17}}$ |  $s_{15}$/10 |  $s_{16}$/10 |  $s_{17}$/10 |  $s_{17}$/10 |  $s_{14}$/11 |  $s_{23}$/10 |  $s_{17}$/10 |  $s_{17}$/10 |  $s_{5}$/10
$\mathbf{s_{18}}$ |  $s_{18}$/10 |  $s_{19}$/10 |  $s_{20}$/10 |  $s_{21}$/10 |  $s_{18}$/10 |  $s_{18}$/10 |  $s_{12}$/00 |  $s_{18}$/10 |  $s_{6}$/10
$\mathbf{s_{19}}$ |  $s_{18}$/10 |  $s_{19}$/10 |  $s_{20}$/10 |  $s_{22}$/10 |  $s_{19}$/10 |  $s_{19}$/10 |  $s_{13}$/11 |  $s_{19}$/10 |  $s_{7}$/10
$\mathbf{s_{20}}$ |  $s_{18}$/10 |  $s_{19}$/10 |  $s_{20}$/10 |  $s_{23}$/10 |  $s_{20}$/10 |  $s_{20}$/10 |  $s_{14}$/11 |  $s_{20}$/10 |  $s_{8}$/10
$\mathbf{s_{21}}$ |  $s_{21}$/10 |  $s_{22}$/10 |  $s_{23}$/10 |  $s_{21}$/10 |  $s_{18}$/10 |  $s_{21}$/10 |  $s_{15}$/10 |  $s_{21}$/10 |  $s_{9}$/10
$\mathbf{s_{22}}$ |  $s_{21}$/10 |  $s_{22}$/10 |  $s_{23}$/10 |  $s_{22}$/10 |  $s_{19}$/10 |  $s_{22}$/10 |  $s_{16}$/10 |  $s_{22}$/10 |  $s_{10}$/10
$\mathbf{s_{23}}$ |  $s_{21}$/10 |  $s_{22}$/10 |  $s_{23}$/10 |  $s_{23}$/10 |  $s_{20}$/10 |  $s_{23}$/10 |  $s_{17}$/10 |  $s_{23}$/10 |  $s_{11}$/10

First column defines the states (initial state $s_{0}$)
First row defines the inputs
Fields $s/y$ denote ‘Post-state/Output’

Inputs:

f0, f1, f2 : FSB switch in position OFF, ON, AUTO

d1, d0 : Cabin decompression true, false

e1, e0 : Excessive altitude true, false

a1, a0 : Auto condition true, false

Outputs:

00 denotes (FSB,RTS)=(0,0)

11 denotes (FSB,RTS)=(1,1)

10 denotes (FSB,RTS)=(1,0)

Table 2: Explanation of states $\mathbf{s_{0}}$,…, $\mathbf{s_{23}}$ in Table 1. |  Cockpit Switch |  Decompression |  Excessive
Altitude |  AUTO
Condition |  Current
Output
---|---|---|---|---|---
$\mathbf{s_{0}}$ |  0 |  0 |  0 |  0 |  00
$\mathbf{s_{1}}$ |  1 |  0 |  0 |  0 |  11
$\mathbf{s_{2}}$ |  2 |  0 |  0 |  0 |  00
$\mathbf{s_{3}}$ |  0 |  1 |  0 |  0 |  10
$\mathbf{s_{4}}$ |  1 |  1 |  0 |  0 |  10
$\mathbf{s_{5}}$ |  2 |  1 |  0 |  0 |  10
$\mathbf{s_{6}}$ |  0 |  0 |  1 |  0 |  10
$\mathbf{s_{7}}$ |  1 |  0 |  1 |  0 |  10
$\mathbf{s_{8}}$ |  2 |  0 |  1 |  0 |  10
$\mathbf{s_{9}}$ |  0 |  1 |  1 |  0 |  10
$\mathbf{s_{10}}$ |  1 |  1 |  1 |  0 |  10
$\mathbf{s_{11}}$ |  2 |  1 |  1 |  0 |  10
$\mathbf{s_{12}}$ |  0 |  0 |  0 |  1 |  00
$\mathbf{s_{13}}$ |  1 |  0 |  0 |  1 |  11
$\mathbf{s_{14}}$ |  2 |  0 |  0 |  1 |  11
$\mathbf{s_{15}}$ |  0 |  1 |  0 |  1 |  10
$\mathbf{s_{16}}$ |  1 |  1 |  0 |  1 |  10
$\mathbf{s_{17}}$ |  2 |  1 |  0 |  1 |  10
$\mathbf{s_{18}}$ |  0 |  0 |  1 |  1 |  10
$\mathbf{s_{19}}$ |  1 |  0 |  1 |  1 |  10
$\mathbf{s_{20}}$ |  2 |  0 |  1 |  1 |  10
$\mathbf{s_{21}}$ |  0 |  1 |  1 |  1 |  10
$\mathbf{s_{22}}$ |  1 |  1 |  1 |  1 |  10
$\mathbf{s_{23}}$ |  2 |  1 |  1 |  1 |  10

A _cabin controller_ in a modern aircraft switches the _fasten seat belt (FSB)
signs_ located above the passenger seats in the cabin and the _return to seat
(RTS) signs_ located in the lavatories according to the rules modelled in the
DFSM shown in Table 1. Note that this DFSM is already minimal.

As inputs, the cabin controller reads the actual position of the fasten seat
belts switch in the cockpit, which has the position f0 (OFF), f1 (ON), and f2
(AUTO). Further inputs come from the cabin pressure control system which
indicates “cabin pressure low” by event d1 and “cabin pressure ok” by d0. This
controller also indicates “excessive altitude” by e1 or “altitude in
admissible range” by e0. Another sub-component of the cabin controller
determines whether the so-called AUTO condition is true (event a1) or false
(a0).

The cabin controller switches the fasten seat belt signs and return to seat
signs on and off, depending on the actual input change and its current
internal state. As long as the cabin pressure and the cruising altitude are ok
(after initialisation of the cabin controller or if last events from the cabin
pressure controller were d0, e0), the status of the FSB and RTS signs is
determined by the cockpit switch and the AUTO condition: if the switch is in
the ON position, both FSB and RTS signs are switched on (output 11 in Table
1). Turning the switch into the OFF position switches the signs off. If the
switch is in the AUTO position, both FSB and RTS signs are switched on if the
AUTO condition becomes true with event a1, and they are switched off again
after event a0. The AUTO condition may depend on the status of landing gears,
slats, flaps, and oil pressure, these details are abstracted to a1, a0 in our
example.

As soon as a loss of pressure occurs in the cabin (event d1) or an excessive
altitude is reached, the FSB signs must be switched on and remain in this
state, regardless of the actual state of the cockpit switch and the AUTO
condition. The RTS signs, however, need to be switched off, because passengers
should not be encouraged to leave the lavatories in a low pressure or
excessive altitude situation.

After the cabin pressure and the altitude are back in the admissible range,
the FSB and RTS signs shall automatically resume their state as determined by
the “normal” inputs from cockpit switch and AUTO condition.

Table 2 facilitates the interpretation of the DFSM model shown in Table 1: for
every DFSM state $\mathbf{s_{0}}$,…,$\mathbf{s_{23}}$, the associated status
of the cockpit switch, cabin decompression, excessive altitude, and AUTO
condition, as well as the last output made when entering the state is
displayed.

###  6.2 Complete Test Suites Checking Model Equivalence Computed by the
H-Method

Applying the H-Method DBLP:conf/forte/DorofeevaEY05  as implemented in the
fsmlib-cpp333see Appendix A for instructions how to use the test case
generation program which is part of the library, the number of test cases
needed to test an implementation to establish language equivalence with full
fault coverage is shown in Table 3, column H. Recall that a test case is a
sequence of inputs. When executing a test case against an implementation, the
expected results are determined As the size of the test suite depends on the
potential number $m$ of implementation states minus the number $n$ of states
in the minimised model, test suites are calculated for $m-n=0,1,2$.

Table 3: Comparison of the numbers of test cases needed to prove
I/O-equivalence (H-Method) and to prove requirements satisfaction using
exhaustive testing for requirements $\mathbf{R}_{1}$ and $\mathbf{R}_{2}$
specified in this section.

$\mathbf{m-n}$ | H | $t_{H}[s]$ | $\mathbf{R}_{1}$ | $\mathbf{\Delta_{1}^{\%}}$ | $t_{1}[s]$ | $\mathbf{R}_{2}$ | $\mathbf{\Delta_{2}^{\%}}$ | $t_{2}[s]$
---|---|---|---|---|---|---|---|---
0 | 518 | 1.3 | 193 | 63 | 0.02 | 337 | 35 | 0.03
1 | 4069 | 76.7 | 1737 | 57 | 0.09 | 3035 | 25 | 0.2
2 | 35325 | 7765.6 | 15633 | 56 | 0.9 | 27327 | 23 | 2.3

Column $\mathbf{m-n}$ contains the maximal difference between the number of
SUT states and model states assumed for the test suite generation. Column H
contains the number of test cases required when using the H-Method for
I/O-equivalence testing. Columns $\mathbf{R}_{i},\ i=1,2$ contain the number
of test cases required for requirements-driven testing of $\mathbf{R}_{i}$.
Columns $\mathbf{\Delta}_{i}^{\%},\ i=1,2$ contain the test case reductions
achieved by requirements-driven testing in percent, calculated according to
formulas $\mathbf{\Delta}_{i}^{\%}=100-100*\frac{R_{i}}{H}$, where $R_{i}$
denotes the number of test cases from column $\mathbf{R}_{i}$ and $H$ the
number from column H. Time $t_{H}$ is the test suite generation time in
seconds needed to create the respective language equivalence test suite using
the H-Method. Durations $t_{i},\ i=1,2$ indicate the time needed to generated
the exhaustive requirements test suites for $\mathbf{R}_{1}$ and
$\mathbf{R}_{2}$, respectively. The time has been measured on an Apple iMac
with 4.2 GHz Intel Core i7 CPU and 64GB 2400 MHz DDR4 memory.

###  6.3 Requirement $\mathbf{R}_{1}$: Safety-relevant outputs on
Decompression

As a first requirement, we consider

> $\mathbf{R}_{1}$. Whenever cabin decompression occurs, the FSB signs shall
> be set to 1, and the RTS signs to 0.

In the DFSM model shown in Table 1, this requirement is reflected by column
$\mathbf{d1}$: regardless of the current state, output (FSB,RTS)=(1,0) is
assigned on occurrence of input $\mathbf{d1}$. Encoding $\mathbf{R}_{1}$ in
our requirements specification formalism results in the following
representation.

$\mathbf{R}_{1}\equiv\bigwedge_{i=0}^{23}R(s_{i},\mathbf{d1},\\{10\\})$

Obviously, the specification of $\mathbf{R}_{1}$ is independent of the current
state, and there are no alternative outputs that may be accepted in exchange
for the output (FSB,RTS)=(1,0) expected according to the reference model.

Creating an exhaustive test suite for $\mathbf{R}_{1}$ according to Theorem
5.1 results in the number of test cases shown in column $\mathbf{R}_{1}$ of
Table 3. As listed in column $\mathbf{\Delta_{1}^{\%}}$ of this table, the
test case reductions achieved in comparison to the H-based test suite vary
with $m-n$ and are in range $56\%$ — $63\%$.

The test of this requirement could be advisable, for example, during
regression testing after the sign controller’s code has been modified with
regard to the sub-function responsible for decompression handling. Instead of
running the complete H-test suite, it would suffice to perform the
significantly smaller test suite for $\mathbf{R}_{1}$ which also guarantees
full fault coverage as far as $\mathbf{R}_{1}$ is concerned.

###  6.4 Requirement $\mathbf{R}_{2}$: All Safety-relevant outputs and Sign
Activation by Manual Switch

As second requirement, we consider a composite requirement related to all
safety-critical events in combination to normal behaviour reactions
(FSB,RTS)=(1,1) when setting the cockpit switch to position 1.

> $\mathbf{R}_{2}$. Whenever cabin decompression or excessive altitude occurs,
> the FSB signs shall be set to 1, and the RTS signs to 0. The signs stay
> activated until both decompression and execessive altitude are no longer
> present. In absence of cabin decompression and excessive altitude, both FSB
> and RTS signs shall be switched on when setting the cockpit switch to
> position 1.

Formalising this requirement leads to

$\displaystyle\mathbf{R}_{2}$ $\displaystyle\equiv$
$\displaystyle\bigwedge_{i=0}^{23}\big{(}R(s_{i},\mathbf{d1},\\{10\\})\wedge
R(s_{i},\mathbf{e1},\\{10\\})\big{)}\wedge{}$
$\displaystyle\bigwedge_{i\in\\{3,\dots,11,15,\dots,23\\}}\big{(}R(s_{i},\mathbf{f0},\\{10\\})\wedge
R(s_{i},\mathbf{f1},\\{10\\})\wedge
R(s_{i},\mathbf{f2},\\{10\\})\big{)}\wedge{}$
$\displaystyle\bigwedge_{i\in\\{3,\dots,11,15,\dots,23\\}}\big{(}R(s_{i},\mathbf{a1},\\{10\\})\wedge
R(s_{i},\mathbf{a0},\\{10\\})\big{)}\wedge{}$
$\displaystyle\bigwedge_{i\in\\{6,\dots,11,18,\dots,23\\}}R(s_{i},\mathbf{d0},\\{10\\})\wedge{}$
$\displaystyle\bigwedge_{i\in\\{3,4,5,9,10,11,15,16,17,21,22,23\\}}R(s_{i},\mathbf{e0},\\{10\\})$
$\displaystyle\bigwedge_{i\in\\{0,1,2,12,13,14\\}}R(s_{i},\mathbf{f1},\\{11\\})$

Creating an exhaustive test suite for $\mathbf{R}_{2}$ according to Theorem
5.1 results in the number of test cases shown in column $\mathbf{R}_{2}$ of
Table 3. As listed in column $\mathbf{\Delta_{2}^{\%}}$ of this table, the
test case reductions achieved in comparison to the H-based test suite are in
range $23\%$ — $35\%$.

Testing this requirement would be advisable, for example, after the initial
development of the sign controller, assuming that there would not be enough
time to perform all tests derived by the H-method. Requirement
$\mathbf{R}_{2}$ leads to a smaller test suite, but still covers all safety-
relevant reactions of the implementation and the most important user
requirement. Then it could be justified to test the functionality related to
the AUTO condition with less effort, since, as a fall back option for the
pilot, signs could always be switched on manually when the AUTO mode is not
properly functioning.

##  7 Complete Testing of Composite Requirements

Suppose that DFSMs $M$ (reference model) and $S$ (implementation) are
completely specified and consider the composite requirement
$R=\bigwedge_{i=1}^{k}R(q_{i},x_{i},Z_{i})$ specified on $M$. In this section,
we are going to construct finite test suites $\text{TS}_{\Leftrightarrow}$
depending on $M$ and $R$ and a new pass relation $\underline{\text{\bf
pass}}_{\Leftrightarrow}$ such that an implementation $S$ passes
$\text{TS}_{\Leftrightarrow}$ if and only if it conforms to the requirements
$R$. In the terminology introduced in Section 1.2, these test suites are
called complete.

###  7.1 A Nondeterministic Alternative to $M_{1}$

Let $M_{1}$ be the FSM abstraction induced by $M$ and $R$ as described in
Section 4. Recall that $M_{1}$ is deterministic with output alphabet
$\\{*,Z_{1},\dots,Z_{k}\\}$, where $*$ is short for $\Sigma_{O}$. The DFSM
$M_{1}$ induces an alternative abstraction $M_{1}^{\prime}$ of $M$, which is
nondeterministic and has output alphabet $\Sigma_{O}$. This nondeterministic
FSM is specified by
$M_{1}^{\prime}=(Q,\underline{q},\Sigma_{I},\Sigma_{O},h_{1}^{\prime})$, where

$(q,x,y,q^{\prime})\in
h_{1}^{\prime}\Leftrightarrow\big{(}\delta_{M_{1}}(q,x)=q^{\prime}\wedge
y\in\omega_{M_{1}}(q,x)\big{)}.$

Given $(q,x)\in\Sigma_{I}\times\Sigma_{I}$ such that $\omega_{M_{1}}(q,x)=*$,
the nondeterministic machine $M_{1}^{\prime}$ possesses the transitions
$(q,x,y,\delta_{M_{1}}(q,x))$ with arbitrary $y\in\Sigma_{O}$. For
$i\in\\{1,\dots,k\\}$, recall that $\omega_{M_{1}}(q_{i},x_{i})=Z_{i}$. For
these cases, $M_{1}^{\prime}$ reacts by nondeterministically taking one of the
transitions $(q_{i},x_{i},y,\delta_{M_{1}}(q,x))$ with $y\in Z_{i}$.

###### Example 5

When representing the abstraction $M_{1}$ from Fig. 3 as a nondeterministic
FSM, this results in $M_{1}^{\prime}$ as depicted in Fig. 5. ∎

Figure 5: Nondeterministic FSM $M_{1}^{\prime}$ created from $M_{1}$ displayed
in Fig. 3.

From the construction rules specified above and from the illustration in
Example 5 and Fig. 5, it is immediately clear that $M_{1}^{\prime}$ is
observable and completely specified. Also note that by construction,
$M_{1}^{\prime}$ may be interpreted as the “most nondeterministic FSM which
still satisfies requirement $R$”: for (state,input)-pairs that are unrelated
to $R$, any output from $\Sigma_{O}$ can occur. For pairs $(q_{i},x_{i})$
related to elementary requirements $R(q_{i},x_{i},Z_{i})$, any output from
$Z_{i}$ can be nondeterministically selected, so that $R(q_{i},x_{i},Z_{i})$
is never violated.

Moreover, $M_{1}^{\prime}$ is only nondeterministic with respect to the
outputs produced in a given state $q$ for a given input $x$, whereas the
target state is uniquely determined by $q$ and $x$. This means that the
transition functions
$\delta_{M_{1}},\delta_{M_{1}^{\prime}}:Q\times\Sigma_{I}\rightarrow Q$ of
$M_{1}$ and $M_{1}^{\prime}$, respectively, coincide in the sense that

$\forall(q,x)\in
Q\times\Sigma_{I}:\delta_{M_{1}}(q,x)=\delta_{M_{1}^{\prime}}(q,x).$

As a consequence, the expressions
$\underline{q}\text{-\text@underline{after}-}\overline{x},\
\overline{x}\in\Sigma_{I}^{*},$ always result in the same uniquely determined
target state, regardless of whether they are evaluated in $M_{1}$ or
$M_{1}^{\prime}$.444Recall that for general nondeterministic FSMs,
$\underline{q}\text{-\text@underline{after}-}\overline{x}$ specifies a set of
possible target states, since their transition relation $h$ may allow for
different target states being reached for a given pre-state and input.

Finally, note that, since $M_{1}^{\prime}$ is nondeterministic, its output
function is set-valued,
$\omega_{M_{1}^{\prime}}:Q\times\Sigma_{I}^{*}\rightarrow\mathbb{P}(\Sigma_{O}^{*})$.
It is easy to see, however, that
$\omega_{M_{1}^{\prime}}(q,x)=\omega_{M_{1}}(q,x)$ for all states $q$ and
inputs $x$: FSM $M_{1}^{\prime}$ has transitions
$q\xrightarrow{x/y}\delta_{M_{1}}(q,x)$ for every $y\in\omega_{M_{1}}(q,x)$.

The following theorem presents an important insight into the relationship
between requirements satisfaction and reduction (i.e. language inclusion): an
implementation machine $S$ satisfies the requirement $R$, if and only if its
language is contained in the language of the abstraction $M_{1}^{\prime}$
constructed above.

###### Theorem 7.1

$S\models R\Leftrightarrow L(S)\subseteq L(M_{1}^{\prime})$

###### Proof

Recall that $\Pi(q)=\\{\overline{x}\in\Sigma_{I}^{*}\leavevmode\nobreak\
|\leavevmode\nobreak\
\underline{q}\text{-\text@underline{after}-}\overline{x}=q\\}$. Also recall
that by definition, $S\models R\Leftrightarrow\forall
i\in\\{1,\dots,k\\},\pi\in\Pi(q_{i}):\omega_{S}(\underline{s}\text{-\text@underline{after}-}\pi,x_{i})\in
Z_{i}$.

Suppose that $L(S)\subseteq L(M_{1}^{\prime})$. Since $S$ is completely
specified by assumption, there exists a unique I/O-trace
$\overline{x}.x_{i}/\overline{y}.y\in L(S)$ for any input sequence
$\overline{x}.x_{i}$ with $\overline{x}\in\Pi(q_{i})$ and
$i\in\\{1,\dots,k\\}$. Since we assume that $S$ is a reduction of
$M_{1}^{\prime}$, this I/O-trace must also be a trace of $M_{1}^{\prime}$. By
construction of $M_{1}^{\prime}$, this means that $y\in Z_{i}$, so $S$ fulfils
requirement $R(q_{i},x_{i},Z_{i})$. Since this argument was independent of
$i\in\\{1,\dots,k\\}$, $S\models R$ follows.

Now suppose that $L(S)\not\subseteq L(M_{1}^{\prime})$. Then there exists an
I/O-trace $\overline{x}.x/\overline{y}.y\in L(S)$ such that
$\overline{x}/\overline{y}\in L(M_{1}^{\prime})$, but
$\overline{x}.x/\overline{y}.y\not\in L(M_{1}^{\prime})$. Suppose that
$(\underline{q}\text{-\text@underline{after}-}\overline{x},x)\neq(q_{i},x_{i})$
for all $i\in\\{1,\dots,k\\}$, where the -after- operator is evaluated in
$M_{1}^{\prime}$. Then, by construction of $M_{1}^{\prime}$,
$\overline{x}.x/\overline{y}.y\in L(M_{1}^{\prime})$ for all $y\in\Sigma_{O}$,
so this is a contradiction to the assumption
$\overline{x}.x/\overline{y}.y\not\in L(M_{1}^{\prime})$.

Thus the assumption $\overline{x}.x/\overline{y}.y\not\in L(M_{1}^{\prime})$
implies the existence of an $i\in\\{1,\dots,k\\}$ such that
$(\underline{q}\text{-\text@underline{after}-}\overline{x},x)=(q_{i},x_{i})$.
As a consequence, $\overline{x}.x_{i}/\overline{y}.y\not\in L(M_{1}^{\prime})$
and $\overline{x}\in\Pi(q_{i})$. By construction of $M_{1}^{\prime}$, this
means that $y\not\in Z_{i}$. This implies that $S$ violates requirement
$R(q_{i},x_{i},Z_{i})$, so $S\not\models R$, and this completes the proof. ∎

###  7.2 The pass criterion $\underline{\text{\bf pass}}_{\Leftrightarrow}$

Let $\overline{x}\in\Sigma_{I}^{*}$ and
$\text{TS}_{\Leftrightarrow}\subseteq\Sigma_{i}^{*}$. We define a new pass
criterion for test cases by

$S\ \underline{\text{\bf pass}}_{\Leftrightarrow}\
\overline{x}\equiv\big{(}\omega_{S}(\underline{s},\overline{x})\in\omega_{M_{1}^{\prime}}(\underline{q},\overline{x})\big{)},$

and extend this to test suites by

$S\ \underline{\text{\bf pass}}_{\Leftrightarrow}\
\text{TS}_{\Leftrightarrow}\equiv\big{(}\forall\overline{x}\in\text{TS}_{\Leftrightarrow}:S\
\underline{\text{\bf pass}}_{\Leftrightarrow}\ \overline{x}\big{)}.$

Intuitively speaking, a test case represented by some input trace
$\overline{x}$ is passed by the implementation $S$ if and only if the
resulting I/O-trace $\overline{x}/\omega_{S}(\underline{s},\overline{x})$
performed by $S$ is contained in the language of $M_{1}^{\prime}$. Using the
respective output functions, this is expressed here by stating that the output
trace generated by $S$ on input trace $\overline{x}$ in an element of the set
of output traces possible in $M_{1}^{\prime}$ for this test case. Therefore,
$\underline{\text{\bf pass}}_{\Leftrightarrow}$ is just the well-known pass
criterion for reduction testing of $S$ against $M_{1}^{\prime}$, that is, for
checking whether $L(S)\subseteq L(M_{1}^{\prime})$ holds.

Figure 6: Implementation $S$ from Example 6.

###### Example 6

At first glance, one might ask whether it is possible to apply the test suites
specified in Theorem 5.1 just with the new pass criterion
$\underline{\text{\bf pass}}_{\Leftrightarrow}$, in order to create complete
test suites for the given requirement. This, however, is not true: the
following example shows that the suites from Theorem 5.1 are no longer
exhaustive, when applied with $\underline{\text{\bf pass}}_{\Leftrightarrow}$.

Consider again reference model $M$ and requirement

$R\equiv R(q_{0},a,\\{0,1\\})\wedge R(q_{1},b,\\{0,2\\})\wedge
R(q_{2},a,\\{0,1\\}).$

from Example 2. From Example 4, we know that

$a.a.b,a.b.b,b.a.b,b.b.a$

is an exhaustive test suite for pass criterion $\underline{\text{\bf
pass}}_{\Rightarrow}$ generated according to rules (14) and (15) from Theorem
5.1. Now consider another implementation $S$ as shown in Fig. 6. Applying the
four test cases above to $S$ results in I/O-traces

$a.a.b/1.1.1,\ a.b.b/1.1.0,\ b.a.b/1.1.0,\ b.b.a/1.0.1$

It is easy to see that $S$ passes the four test cases when applying pass
criterion $\underline{\text{\bf pass}}_{\Leftrightarrow}$ (just check the
observed outputs against $M_{1}$ from Fig. 3). However, $S$ does not satisfy
requirement $R(q_{1},b,\\{0,2\\})$, and, equivalently, $S$ is not a reduction
of $M_{1}^{\prime}$ shown in Fig. 5: input trace $b.a.a.b$ applied to $S$
results in

$b.a.a.b/1.1.0.1,$

but<EMAIL_ADDRESS>in $M$, and
$R(q_{1},b,\\{0,2\\})$ only allows $0$ or $2$ as output when $b$ is applied in
state $q_{1}$. In contrast to that, $S$ outputs 1 when given input $b$ in
state<EMAIL_ADDRESS>Expressed in an
equivalent way, $b.a.a.b/1.1.0.1\not\in L(M_{1}^{\prime})$, for
$M_{1}^{\prime}$ shown in Fig. 5. ∎

###  7.3 Main Theorem on Complete Test Suites

The following theorem shows that any complete test suite for reduction testing
against $M_{1}^{\prime}$ can be reduced in a specific way that still
guarantees requirements satisfaction if and only if the resulting suite is
passed.

###### Theorem 7.2

Let TS be any complete reduction test suite guaranteeing $L(S)\subseteq
L(M_{1}^{\prime})$ if and only if $S\ \underline{\text{\bf
pass}}_{\Leftrightarrow}\text{TS}$ for all $S\in{\cal D}$. Define

$\overline{\Pi}=\bigcup_{i=1}^{k}\Pi(q_{i}).\\{x_{i}\\}.$

Then any test suite $\text{TS}_{\Leftrightarrow}$ satisfying

$\text{pref}(TS)\cap\overline{\Pi}\subseteq\text{TS}_{\Leftrightarrow}$

is complete for testing $R$, that is,

$S\ \underline{\text{\bf pass}}_{\Leftrightarrow}\
\text{TS}_{\Leftrightarrow}\Leftrightarrow S\models R$

holds for all $S\in{\cal D}$, that is, $\text{TS}_{\Leftrightarrow}$ is a
complete suite for testing composite requirement $R$.

###### Proof

Let $\overline{x}\in\Sigma_{I}^{*}$ be any nonempty input sequence and
$\overline{y}=\omega_{S}(\underline{s},\overline{x})$. Let
$\ell=|\overline{x}|=|\overline{y}|$. We prove the following derivation for an
arbitrary test case $\overline{x}$ of the complete reduction test suite TS and
its pass criterion $\underline{\text{\bf pass}}_{\Leftrightarrow}$.

$\displaystyle S\ \underline{\text{\bf pass}}_{\Leftrightarrow}\ \overline{x}$
(17) $\displaystyle\Leftrightarrow$ $\displaystyle\forall
j\in\\{1,\dots,\ell\\}:\overline{y}(j)\in\omega_{M_{1}^{\prime}}(\underline{q}\text{-\text@underline{after}-}\overline{x}^{[1..j-1]},\overline{x}(j))$
(19) $\displaystyle\Leftrightarrow$ $\displaystyle\forall
j\in\\{1,\dots,\ell\\},\big{(}\underline{q}\text{-\text@underline{after}-}\overline{x}^{[1..j-1]},\overline{x}(j)\big{)}\in\\{(q_{i},x_{i})\leavevmode\nobreak\
|\leavevmode\nobreak\ i=1,\dots,k\\}:$
$\displaystyle\overline{y}(j)\in\omega_{M_{1}^{\prime}}(\underline{q}\text{-\text@underline{after}-}\overline{x}^{[1..j-1]},\overline{x}(j))$
$\displaystyle\Leftrightarrow$ $\displaystyle S\ \underline{\text{\bf
pass}}_{\Leftrightarrow}\ \text{pref}(\overline{x})\cap\overline{\Pi}$ (20)

The equivalence (17) $\Leftrightarrow$ (19) follows from re-writing the
original definition of $\underline{\text{\bf pass}}_{\Leftrightarrow}$ with
explicit indexes for input and output events. Implication (19) $\Rightarrow$
(19) is trivial, since we restrict the $\overline{y}(j)$ under consideration
to those that are outputs obtained when applying requirements-related inputs
$x_{i}$ in state $q_{i}$. Conversely, (19) $\Leftarrow$ (19) follows from the
fact that for
$\big{(}\underline{q}\text{-\text@underline{after}-}\overline{x}^{[1..j-1]},\overline{x}(j)\big{)}\not\in\\{(q_{i},x_{i})\leavevmode\nobreak\
|\leavevmode\nobreak\ i=1,\dots,k\\}$, we have
$\omega_{M_{1}^{\prime}}(\underline{q}\text{-\text@underline{after}-}\overline{x}^{[1..j-1]},\overline{x}(j))=\Sigma_{O}$,
so any output is acceptable. Finally, equivalence (19) $\Leftrightarrow$ (20)
follows from the fact that (19) is just the definition of $S\
\underline{\text{\bf pass}}_{\Leftrightarrow}\
\text{pref}(\overline{x})\cap\overline{\Pi}$ with explicit indexes.

With the derivation above, we have shown that in order to prove $L(S)\subseteq
L(M_{1}^{\prime})$, it suffices to check just the test cases
$\text{pref}(\overline{x})\cap\overline{\Pi}$ for all $\overline{x}$ in the
original complete test suite TS. This proves

$L(S)\subseteq L(M_{1}^{\prime})\Leftrightarrow S\ \underline{\text{\bf
pass}}_{\Leftrightarrow}\ \text{TS}_{\Leftrightarrow}.$

Now Theorem 7.1 can be applied to conclude that $S\models R\Leftrightarrow S\
\underline{\text{\bf pass}}_{\Leftrightarrow}\ \text{TS}_{\Leftrightarrow}$,
and this completes the proof. ∎

###### Example 7

Applying the adaptive state counting algorithm from hierons_testing_2004  to
reference model $M_{1}^{\prime}$ from Example 5 and implementation model $S$
from Example 2, a test suite TS with 39 test cases of maximal length is
obtained to test for reduction of $S$ against $M_{1}^{\prime}$ with $n=2$ for
the number of states in the minimised observable FSM associated with
$M_{1}^{\prime}$, and $m=3$ for the number of states in the minimised version
of $S$ (which is identical to $S$).

Restricting this complete reduction test suite to the test cases that are also
contained in $\text{pref}(TS)\cap\overline{\Pi}$, where $\overline{\Pi}$ is
specified according to Theorem 7.2 for reference model $M$ and requirement $R$
specified in Example 2, results in 16 test cases

$\begin{array}[]{llll}a.a.a&a.b.b.b.b&b.a.b.b.b.a&b.b.b.a.b.a\\\
a.a.b.a.b&b.a.a.b.a.a&b.b.a.a&b.b.b.b.a\\\
a.b.a.b.a&b.a.b.a.a&b.b.a.b.a.b&b.b.b.b.b.b\\\
a.b.b.a&b.a.b.a.b.b&b.b.a.b.b&a.a.b.b\end{array}$

It is easy to see that $S$ passes this test suite when applying pass criterion
$\underline{\text{\bf pass}}_{\Leftrightarrow}$ and reference model
$M_{1}^{\prime}$. Moreover, the decrease of test cases in comparison to the
full reduction test suite is significant. However, observing that the
exhaustive test suite for checking requirements satisfaction according to
Theorem 5.1 needs only 4 test cases (see Example 4), shows at least for this
example that complete requirements testing needs far more test cases than
exhaustive requirements testing. This observation will be discussed in more
detail in the next section. ∎

##  8 Complexity Considerations

###  8.1 Maximal Length of Test Cases

#### Exhaustive requirements testing.

Consider first the maximal length $\text{tcl}_{max}^{exh}$ of test cases for
exhaustive requirements testing according to Theorem 5.1. From the test suite
specification in (14) and (15), we conclude that

$\displaystyle\text{tcl}_{max}^{exh}$ $\displaystyle\leq$
$\displaystyle\text{`maximal length of traces in $V$'}+{}$ $\displaystyle
m-n+1+{}$ ‘maximal length of distinguishing traces $\gamma$’

When using state covers $V$ with minimal-length input traces, the latter are
bounded by $n-1$, where $n$ is the number of states in the prime machine of
the reference model. Also, minimal-length distinguishing traces are bounded by
$n-1$. This gives us an upper bound

$\text{tcl}_{max}^{exh}\leq n+m-1$ (22)

for the maximal test case length. For Example 4, the state cover has traces of
maximal length 1, and the minimal-length distinguishing traces have length 1.
Moreover, $m=n=3$. Applying Formula (8.1) results in
$\text{tcl}_{max}^{exh}=3$, and this is confirmed by the test traces
calculated in Example 4 that are all of length 3.

#### Complete requirements testing.

It is well known that testing for language equivalence requires shorter test
cases than testing for reduction. This is discussed, for example, in the
lecture notes PeleskaHuangLectureNotesMBT : there, it is shown that for
certain reference models, any complete reduction test suite needs test cases
of maximal length

$\text{tcl}_{max}^{cmp}=m\cdot n,$

where $m$ is the maximal number of SUT states, and $n$ the number of states in
the minimised observable reference model (PeleskaHuangLectureNotesMBT, ,
Section 4.5). This is reflected by Example 7, where $m=3$ and $n=2$ (number of
states in the prime machine of $M_{1}^{\prime}$), and the longest test case
has $m\cdot n=6$ inputs.

###  8.2 Maximal Number of Test Cases

When calculating upper bounds for the number of test cases needed in an
exhaustive or complete test suite, test cases that are prefixes of others can
be removed from the suite: if an input traces $\overline{x}_{1}$ reveals an
error in the implementation, then this error will also be revealed by any
longer input traces $\overline{x}_{1}.\overline{x}_{2}$ which has
$\overline{x}_{1}$ as prefix. The bounds presented here take this observation
into account.

#### Exhaustive requirements testing.

The maximal number $\text{tc}_{max}^{exh}$ of test cases for exhaustive
requirements testing coincides with the maximal number of test cases needed
for language equivalence testing, since, when choosing requirement $R_{eq}$
specified in Theorem 3.1, this characterises language equivalence.

As a consequence, the estimate $\text{tc}_{max}^{exh}$ for exhaustive
requirements testing according to Theorem 5.1 is that of the H-method. As
pointed out by the inventors of the H-Method in DBLP:conf/forte/DorofeevaEY05
, the upper bound depends on the implementation technique for the method in a
critical way. Based on experiments made in DBLP:conf/forte/DorofeevaEY05  and
on our implementation in the fsmlib-cpp, the H-Method usually requires
significantly fewer test cases than the well-known W-Method, for which the
upper bound $n^{2}\cdot|\Sigma_{I}|^{m-n+1}$ is well-known vasilevskii1973 ;
chow:wmethod . As a consequence, it is safe to assume that test suites created
by the H-Method fulfil

$\text{tc}_{max}^{exh}\leq n^{2}\cdot|\Sigma_{I}|^{m-n+1}$ (23)

#### Complete requirements testing.

For complete requirements testing according to Theorem 7.1 and Theorem 7.2,
the maximal number $\text{tc}_{max}^{cmp}$ of test cases required is the
maximal number required for reduction testing, where the reduction test suite
is generated from the nondeterministic abstraction $M_{1}^{\prime}$ created
from the original reference model $M$ and the requirement $R$ as described in
Section 7.1. We assume that the minimised equivalent of $M_{1}^{\prime}$ has
$n$ states. Any complete reduction testing strategy can be used for this
purpose, and from the resulting test suites TS, all input traces outside
$\text{pref}(\text{TS})\cap\overline{\Pi}$ can be removed, as shown in Theorem
7.2.

A very basic strategy derived from an investigation of product automata shows
that the set $\Sigma_{I}^{nm}$ of all input sequences of length $m\cdot n$ is
a complete reduction test suite (see, for example, the lecture notes
(PeleskaHuangLectureNotesMBT, , Section 4.5)).

For most practical examples, (adaptive) state counting methods as published in
petrenko_testing_2011 ; DBLP:conf/hase/PetrenkoY14 ; hierons_testing_2004
need significantly fewer test cases that $|\Sigma_{I}^{nm}|$. In the general
case, however, they may perform even worse than this bound derived from
product automata. Fortunately, Theorem 7.2 deals with deterministic
implementations only, and the specific structure of the nondeterministic
reference models $M_{1}^{\prime}$ introduced in Section 7.1 guarantees that
every state is _deterministically reachable_ in the sense that we can
calculate state covers as in the deterministic case, where every input trace
is guaranteed to lead to the specified target state – only the outputs
accompanying this input trace may vary nondeterministically. As a consequence,
there exists a deterministic state cover $V$ of $M_{1}^{\prime}$ with $n$
elements whose traces have bounded length less or equal to $n-1$. A standard
argument from state counting methods (see references above) now implies that
test suites of the form

$V.\bigcup_{i=0}^{mn-n+1}\Sigma_{I}^{i}$

are complete for checking language inclusion. Observing that $|V|=n$ and
prefixes of other test cases can be removed from a test suite without
impairing its completeness properties, this results in the upper bound

$\text{tc}_{max}^{cmp}=n\cdot|\Sigma_{I}|^{mn-n+1},$ (24)

for the number of test cases needed to check whether the SUT is a reduction of
$M_{1}^{\prime}$.

###  8.3 Discussion of Bounds for the Number of Test Cases

Comparing the dominating values in formulas (23) and (24), we find that the
exhaustive strategy is only exponential in the difference $m-n$, whereas the
complete strategy is exponential in the product $m\cdot(n-1)$. This confirms
the observation from Example 7 that complete requirements testing needs
considerably more test cases that the exhaustive strategy.

From a practical perspective, it will be useful in most situations to learn
additional errors about violations of language equivalence, even if they do
not represent violations of requirements. The disadvantage of having to debug
whether a failed test case points to a requirements violation or “only” to a
general violation of language equivalence seems of lesser importance to us
than the fact that the exhaustive strategy needs fewer test cases.

##  9 Related Work

The use of formal specifications, in particular, reference models with formal
behavioural semantics, has a long tradition in testing
DBLP:journals/csur/HieronsBBCDDGHKKLSVWZ09 ; Petrenko:2012:MTS:2347096.2347101
; DBLP:journals/jss/AnandBCCCGHHMOE13 . Among the numerous formal approaches,
complete test strategies have received special attention, because they
guarantee full fault coverage with respect to a reference model and a
conformance relation under certain well-defined hypotheses concerning the
potential faults of the system under test (SUT). Complete strategies are of
particular interest in the domain of safety-critical systems, where a
justification of the test case selection is required in order to obtain
certification credit. These strategies have been comprehensively investigated
in the context of conformance testing. Typical conformance relations were
I/O-language equivalence or language containment vasilevskii1973 ;
chow:wmethod ; DBLP:conf/forte/DorofeevaEY05 ; DBLP:conf/forte/DorofeevaEY05 ;
simao_reducing_2012 ; hierons_testing_2004 ; petrenko_testing_2011 ;
peleska_sttt_2014 , refinement relations for process algebras and related
formalisms DBLP:conf/icfem/CavalcantiG07 ; DBLP:journals/acta/CavalcantiG11 ,
and the well-known ioco-relation tretmans1996 . In the context of hybrid
systems, new conformance relations have been proposed, for example, in
DBLP:journals/scp/AraujoCMMS18 .

Theorem 7.2 states that any complete reduction test suite can be modified to
yield a (usually smaller) complete suite for requirements testing. Typical
complete reduction testing strategies are based on a _state counting_ method;
these are essential for testing reduction relations between nondeterministic
reference models and (deterministic or nondeterministic) SUTs. State counting
has been explained in hierons_testing_2004 ; petrenko_testing_2011 . The fact
that reduction (in our case, the reduction of a model abstraction
$M_{1}^{\prime}$ presented in Section 7.1) preserves requirements satisfaction
is a very general insight which holds for different modelling formalisms and
requirements specification methods. We refer here the well-known fact that LTL
specifications can be checked by a maximally nondeterministic Buchi automaton
and all refinements thereof fulfil the formula as well
DBLP:books/daglib/0020348 . The Unified Theories of Programming hoare1998
investigate both requirements satisfaction and refinement on a more general
logical level and provide the insight that refinement is strongly related to
logical implication. Therefore, requirements satisfaction is preserved by
refinement as a simple logical consequence.

While conformance testing is preferred in the field of protocol verification
protocoltestsystems95 ; DBLP:conf/pts/TretmansKB91 , other application areas
follow the property-driven approach, where it has to be established that the
SUT implements a collection of requirements in a correct way
machado_towards_2007 ; DBLP:conf/fates/FernandezMP03 ; DBLP:conf/soqua/LiQ04 ;
reqbasedtestingskokovic ; DBLP:conf/isola/0001BH18 . Again, models reflecting
the requirements under consideration may be used. Alternatively, implicit
specifications in linear temporal logic can be constructed to identify the
I/O-traces fulfilling a requirement; the underlying theory has been
elaborated, for example, in (DBLP:books/daglib/0020348, , Section 4.2) and
Safra:1988:COA:1398513.1398627 . Since logic specifications referring to the
interfaces of the SUT alone can become very complex, it is often advocated to
combine models with temporal logic specifications, so that the latter may also
refer to internal states of the model, thereby simplifying the formulae
DBLP:conf/ets/Peleska18 ; DBLP:conf/isola/0001BH18 .

When applied to complex real-world systems, complete FSM-based testing methods
usually require very large test suites. This problem has been mitigated in
recent years by abstraction techniques based on equivalence classes and
symbolic state machines, see, for example, Huang2017 ;
DBLP:conf/models/Petrenko18 : the original FSM-based test generation
algorithms can be applied to abstractions of more complex models, such as
extended finite state machines or UML state machines. Examples presented in
DBLP:conf/rssrail/PeleskaHH16  show that these abstraction techniques allow
for complete testing of quite complex control systems with feasible effort.

##  10 Conclusion

In this paper, a notion for specifying elementary and composite requirements
in deterministic finite state machine models has been defined. Two black-box
testing strategies proving or disproving that an implementation satisfies
these requirements have been presented. The first is exhaustive in the sense
that every implementation violating the requirement will fail at least one
test case generated according to the strategy. Failing a test case implies
that the SUT is not language equivalent to the reference model, but may not
necessarily mean that the implementation violates the requirement. The second
is complete in the sense that it is exhaustive and guarantees that failing a
test case alway implies that the system under test violates the requirement.
The exhaustiveness and completeness properties, respectively, of the test
suites generated according to these strategies hold under the assumption that
the implementation has no more than $m\geq n$ states, where $n$ is the known
number of states in the reference model.

The implementation of the first strategy is based on the H-method. Using a
real-world application, it is demonstrated that the first strategy frequently
requires significantly less test cases than a complete method establishing
language equivalence by means of the original H-method. Therefore, the new
method is well-suited for testing a selection of critical requirements with
guaranteed fault coverage, while less critical requirements can be tested in
the conventional way, using heuristics for test case generation.

The implementation of the second strategy is based on a state counting method
which has been originally used to test for language inclusion. While the
second strategy leads to smaller test suites in comparison to complete methods
showing language inclusion, it usually results in more test cases than needed
for establishing language equivalence. Consequently, it is of more theoretical
interest, at least if a model can be constructed that is equivalent to the
desired behaviour of the implementation.

###### Acknowledgements.

The authors would like to thank Robert Sachtleben for pointing out important
details about the complexity of state counting methods.

## References

  * (1) Anand, S., Burke, E.K., Chen, T.Y., Clark, J.A., Cohen, M.B., Grieskamp, W., Harman, M., Harrold, M.J., McMinn, P.: An orchestrated survey of methodologies for automated software test case generation.  Journal of Systems and Software 86(8), 1978–2001 (2013)
  * (2) Araujo, H.L.S., Carvalho, G., Mohaqeqi, M., Mousavi, M.R., Sampaio, A.: Sound conformance testing for cyber-physical systems: Theory and implementation.  Sci. Comput. Program. 162, 35–54 (2018).  DOI 10.1016/j.scico.2017.07.002.  URL https://doi.org/10.1016/j.scico.2017.07.002
  * (3) Baier, C., Katoen, J.: Principles of model checking.  MIT Press (2008)
  * (4) Cavalcanti, A., Gaudel, M.: Testing for refinement in CSP.  In: M.J. Butler, M.G. Hinchey, M.M. Larrondo-Petrie (eds.) Formal Methods and Software Engineering, 9th International Conference on Formal Engineering Methods, ICFEM 2007, Boca Raton, FL, USA, November 14-15, 2007, Proceedings, _Lecture Notes in Computer Science_ , vol. 4789, pp. 151–170. Springer (2007).  DOI 10.1007/978-3-540-76650-6“˙10.  URL https://doi.org/10.1007/978-3-540-76650-6\\_10
  * (5) Cavalcanti, A., Gaudel, M.C.: Testing for refinement in circus.  Acta Inf. 48(2), 97–147 (2011)
  * (6) CENELEC: EN 50128:2011 Railway applications - Communication, signalling and processing systems - Software for railway control and protection systems (2011)
  * (7) Chow, T.S.: Testing software design modeled by finite-state machines.  IEEE Transactions on Software Engineering SE-4(3), 178–186 (1978)
  * (8) Dorofeeva, R., El-Fakih, K., Yevtushenko, N.: An improved conformance testing method.  In: F. Wang (ed.) Formal Techniques for Networked and Distributed Systems - FORTE 2005, 25th IFIP WG 6.1 International Conference, Taipei, Taiwan, October 2-5, 2005, Proceedings, _Lecture Notes in Computer Science_ , vol. 3731, pp. 204–218. Springer (2005).  DOI 10.1007/11562436˙16.  URL https://doi.org/10.1007/11562436_16
  * (9) Fernandez, J., Mounier, L., Pachon, C.: Property oriented test case generation.  In: A. Petrenko, A. Ulrich (eds.) Formal Approaches to Software Testing, Third International Workshop on Formal Approaches to Testing of Software, FATES 2003, Montreal, Quebec, Canada, October 6th, 2003, _Lecture Notes in Computer Science_ , vol. 2931, pp. 147–163. Springer (2003).  DOI 10.1007/978-3-540-24617-6˙11.  URL https://doi.org/10.1007/978-3-540-24617-6_11
  * (10) Hierons, R.M.: Testing from a nondeterministic finite state machine using adaptive state counting.  IEEE Trans. Computers 53(10), 1330–1342 (2004).  DOI 10.1109/TC.2004.85.  URL http://doi.ieeecomputersociety.org/10.1109/TC.2004.85
  * (11) Hierons, R.M., Bogdanov, K., Bowen, J.P., Cleaveland, R., Derrick, J., Dick, J., Gheorghe, M., Harman, M., Kapoor, K., Krause, P.J., Lüttgen, G., Simons, A.J.H., Vilkomir, S.A., Woodward, M.R., Zedan, H.: Using formal specifications to support testing.  ACM Comput. Surv. 41(2), 9:1–9:76 (2009).  DOI 10.1145/1459352.1459354.  URL https://doi.org/10.1145/1459352.1459354
  * (12) Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming.  Prentice-Hall (1998)
  * (13) Huang, W., Peleska, J.: Complete model-based equivalence class testing.  Software Tools for Technology Transfer 18(3), 265–283 (2016).  DOI 10.1007/s10009-014-0356-8.  URL http://dx.doi.org/10.1007/s10009-014-0356-8
  * (14) Huang, W., Peleska, J.: Safety-complete test suites.  In: N. Yevtushenko, A.R. Cavalli, H. Yenigün (eds.) Testing Software and Systems - 29th IFIP WG 6.1 International Conference, ICTSS 2017, St. Petersburg, Russia, October 9-11, 2017, Proceedings, _Lecture Notes in Computer Science_ , vol. 10533, pp. 145–161. Springer (2017).  DOI 10.1007/978-3-319-67549-7˙9.  URL https://doi.org/10.1007/978-3-319-67549-7_9
  * (15) Huang, W.l., Özoguz, S., Peleska, J.: Safety-complete test suites.  Software Quality Journal (2018).  DOI 10.1007/s11219-018-9421-y.  Https://doi.org/10.1007/s11219-018-9421-y
  * (16) Huang, W.l., Peleska, J.: Complete model-based equivalence class testing for nondeterministic systems.  Formal Aspects of Computing 29(2), 335–364 (2017).  DOI 10.1007/s00165-016-0402-2.  URL http://dx.doi.org/10.1007/s00165-016-0402-2
  * (17) Li, S., Qi, Z.: Property-oriented testing: An approach to focusing testing efforts on behaviours of interest.  In: S. Beydeda, V. Gruhn, J. Mayer, R.H. Reussner, F. Schweiggert (eds.) Testing of Component-Based Systems and Software Quality, Proceedings of SOQUA 2004 (First International Workshop on Software Quality) and TECOS 2004 (Workshop Testing Component-Based Systems), _LNI_ , vol. 58, pp. 191–206. GI (2004).  URL http://subs.emis.de/LNI/Proceedings/Proceedings58/article3512.html
  * (18) Luo, G., Bochmann, G., Petrenko, A.: Test selection based on communicating nondeterministic finite-state machines using a generalized wp-method.  IEEE Trans. Software Eng. 20(2), 149–162 (1994).  DOI 10.1109/32.265636.  URL http://doi.ieeecomputersociety.org/10.1109/32.265636
  * (19) Machado, P.D.L., Silva, D.A., Mota, A.C.: Towards Property Oriented Testing.  Electronic Notes in Theoretical Computer Science 184(Supplement C), 3–19 (2007).  DOI 10.1016/j.entcs.2007.06.001.  URL http://www.sciencedirect.com/science/article/pii/S157106610700432X
  * (20) Mizuno, T., Higashino, T., Shiratori, N. (eds.): Protocol Test Systems, 7th workshop 7th IFIP WG 6.1 international workshop on protocol text systems.  IFIP Advances in Information and Communication Technology. Springer Science+Business Media Dordrecht (1995)
  * (21) Object Management Group: OMG Systems Modeling Language (OMG SysML), Version 1.5.  Tech. rep., Object Management Group (2017).  Http://www.omg.org/spec/SysML/1.5
  * (22) Peleska, J.: Model-based avionic systems testing for the airbus family.  In: 23rd IEEE European Test Symposium, ETS 2018, Bremen, Germany, May 28 - June 1, 2018, pp. 1–10. IEEE (2018).  DOI 10.1109/ETS.2018.8400703.  URL https://doi.org/10.1109/ETS.2018.8400703
  * (23) Peleska, J., Brauer, J., Huang, W.: Model-based testing for avionic systems proven benefits and further challenges.  In: T. Margaria, B. Steffen (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice - 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part IV, _Lecture Notes in Computer Science_ , vol. 11247, pp. 82–103. Springer (2018).  DOI 10.1007/978-3-030-03427-6“˙11.  URL https://doi.org/10.1007/978-3-030-03427-6\\_11
  * (24) Peleska, J., Huang, W.: Test Automation - Foundations and Applications of Model-based Testing.  University of Bremen (2019).  URL http://www.informatik.uni-bremen.de/agbs/jp/papers/test-automation-huang-peleska.pdf.  Lecture notes
  * (25) Peleska, J., Huang, W., Hübner, F.: A novel approach to HW/SW integration testing of route-based interlocking system controllers.  In: T. Lecomte, R. Pinger, A. Romanovsky (eds.) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification - First International Conference, RSSRail 2016, Paris, France, June 28-30, 2016, Proceedings, _Lecture Notes in Computer Science_ , vol. 9707, pp. 32–49. Springer (2016).  DOI 10.1007/978-3-319-33951-1˙3.  URL http://dx.doi.org/10.1007/978-3-319-33951-1_3
  * (26) Petrenko, A.: Towards testing from finite state machines with symbolic inputs and outputs.  In: A. Wasowski, R.F. Paige, Ø. Haugen (eds.) Proceedings of the 21th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2018, Copenhagen, Denmark, October 14-19, 2018, p. 187. ACM (2018).  DOI 10.1145/3239372.3242894.  URL https://doi.org/10.1145/3239372.3242894
  * (27) Petrenko, A., Simao, A., Maldonado, J.C.: Model-based testing of software and systems: Recent advances and challenges.  Int. J. Softw. Tools Technol. Transf. 14(4), 383–386 (2012).  DOI 10.1007/s10009-012-0240-3.  URL http://dx.doi.org/10.1007/s10009-012-0240-3
  * (28) Petrenko, A., Yevtushenko, N.: Adaptive testing of deterministic implementations specified by nondeterministic fsms.  In: Testing Software and Systems, no. 7019 in Lecture Notes in Computer Science, pp. 162–178. Springer, Berlin, Heidelberg (2011)
  * (29) Petrenko, A., Yevtushenko, N.: Adaptive testing of nondeterministic systems with FSM.  In: 15th International IEEE Symposium on High-Assurance Systems Engineering, HASE 2014, Miami Beach, FL, USA, January 9-11, 2014, pp. 224–228. IEEE Computer Society (2014).  DOI 10.1109/HASE.2014.39.  URL http://dx.doi.org/10.1109/HASE.2014.39
  * (30) RTCA SC-205/EUROCAE WG-71: Software Considerations in Airborne Systems and Equipment Certification.  Tech. Rep. RTCA/DO-178C, RTCA Inc, 1140 Connecticut Avenue, N.W., Suite 1020, Washington, D.C. 20036 (2011)
  * (31) Safra, S.: On the complexity of omega-automata.  In: Proceedings of the 29th Annual Symposium on Foundations of Computer Science, SFCS ’88, pp. 319–327. IEEE Computer Society, Washington, DC, USA (1988).  DOI 10.1109/SFCS.1988.21948.  URL https://doi.org/10.1109/SFCS.1988.21948
  * (32) Simão, A., Petrenko, A., Yevtushenko, N.: On reducing test length for FSMs with extra states.  Software Testing, Verification and Reliability 22(6), 435–454 (2012).  DOI 10.1002/stvr.452.  URL https://onlinelibrary.wiley.com/doi/abs/10.1002/stvr.452
  * (33) Skoković, P., Rakić-Skoković, M.: Requirements-based testing process in practice.  International Journal of Industrial Engineering and Management (IJIEM) 1(4), 155 – 161 (2010)
  * (34) Starke, P.H.: Abstract Automata.  Elsevier, North-Holland, Amsterdam (1972)
  * (35) Tretmans, J.: Conformance testing with labelled transition systems: Implementation relations and test generation.  Computer Networks and ISDN Systems 29(1), 49–79 (1996)
  * (36) Tretmans, J.: Test generation with inputs, outputs and repetitive quiescence.  Software-Concepts and Tools 17, 103–120 (1996)
  * (37) Tretmans, J., Kars, P., Brinksma, E.: Protocol conformance testing: A formal perspective on ISO IS-9646.  In: J. Kroon, R.J. Heijink, E. Brinksma (eds.) Protocol Test Systems, IV, Proceedings of the IFIP TC6/WG6.1 Fourth International Workshop on Protocol Test Systems, Leidschendam, The Netherlands, 15-17 October, 1991, _IFIP Transactions_ , vol. C-3, pp. 131–142. North-Holland (1991)
  * (38) Vasilevskii, M.P.: Failure diagnosis of automata.  Kibernetika (Transl.) 4, 98–108 (1973)
  * (39) Whalen, M.W., Rajan, A., Heimdahl, M.P.E., Miller, S.P.: Coverage metrics for requirements-based testing.  In: L.L. Pollock, M. Pezzè (eds.) Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2006, Portland, Maine, USA, July 17-20, 2006, pp. 25–36. ACM (2006).  DOI 10.1145/1146238.1146242.  URL https://doi.org/10.1145/1146238.1146242

##  Appendix A Tool Support and Resources

The test suites presented in the examples above have been generated using the
open source library fsmlib-cpp. The library is downloaded, compiled, and some
executables are created according to the instructions given in
(PeleskaHuangLectureNotesMBT, , Appendix B). After that, an executable fsm-
generator is available which allows for test suite generation according to
various strategies without having to write own main programs accessing the
library classes and their methods.

Reference model $M$ and SUT model $S$ from Example 2 can be found in the
fsmlib-cpp installation, directory

    resources/complete-requirements-based-testing/Example-2-3-4

as files M.csv and S.csv, respectively (deterministic FSMs can be specified in
CSV format as explained in (PeleskaHuangLectureNotesMBT, , Appendix B)).

To re-generate the H-method test suite checking language equivalence as
described in Example 4, change into the Example-2-3-4-directory and type
command

    <path-to-executable>/fsm-generator -h -a 0 M.csv

Option -a specifies the maximal number of additional states allowed in the
SUT, so this generation creates an H-test suite from $M$ which is complete for
language equivalence testing under the assumption that $S$ does not have more
states than $M$.

For generating the exhaustive requirements test suite from $M$ and $R$
according to Example 4, the abstraction $M_{1}$ has to be manually created
from $M$ and $R$ as specified in Example 2. This DFSM is also stored in the
Example-2-3-4 directory as file M1.csv. The exhaustive requirements test suite
is now generated by command

    <path-to-executable>/fsm-generator -s -h -a 0 M.csv M1.csv

The -s parameter specifies requirements-based testing, and in such a case, a
second FSM specification file (here: M1.csv) is expected as parameter. This
call to the generator creates exactly the test suite with the 4 test cases
shown in Example 4 for requirements-based testing according to Theorem 5.1.

For generating the test suites related to the Fasten-Seat-Belt and Return-to-
Seat-Sign controller described in Section 6, change into directory

    resources/complete-requirements-based-testing/Section-6

The reference model described in Section 6 is stored in this directory as
FSBRTSX.csv (note that the csv-file uses other state names than the $s_{i}$
shown in Table 1). The DFSM abstraction created from requirement
$\mathbf{R}_{1}$ is contained in file FSBRTSX-ABS-R1.csv. To re-create the
test suites for different values of $m-n$ as specified in Table 3, column
$\mathbf{R}_{1}$, use commands

    <path-to-executable>/fsm-generator -s -h -a 0 FSBRTSX.csv FSBRTSX-ABS-R1.csv
    <path-to-executable>/fsm-generator -s -h -a 1 FSBRTSX.csv FSBRTSX-ABS-R1.csv
    <path-to-executable>/fsm-generator -s -h -a 2 FSBRTSX.csv FSBRTSX-ABS-R1.csv

For requirement $\mathbf{R}_{2}$ specified in Section 6, use abstraction file
file FSBRTSX-ABS-R2.csv and commands that are equivalent to the ones shown
above. To create the complete test suites for language equivalence with the
H-Method, use commands

    <path-to-executable>/fsm-generator -h -a 0 FSBRTSX.csv
    <path-to-executable>/fsm-generator -h -a 1 FSBRTSX.csv
    <path-to-executable>/fsm-generator -h -a 2 FSBRTSX.csv