Exhaustive Property Oriented Model-Based Testing with Symbolic Finite State Machines

Abstract

In this paper, we present new contributions to property oriented testing (POT) against Symbolic Finite State Machine (SFSM) models. While several POT approaches are known, none of these are exhaustive in the sense that every implementation violating the property is uncovered by a given test suite under certain hypotheses. On the other hand, numerous exhaustive theories for testing against models specified in various formalisms exist, but only for conformance testing. Since a hybrid approach using both models and properties seems to be preferred in industry, we present an approach to close this gap. For given properties that are at the same time represented in a reference model, we present a test suite derivation procedure and prove its exhaustiveness.

Funded by the Deutsche Forschungsgemeinschaft (DFG) – project number 407708394.

1 Introduction

Background: Property-Oriented Testing and Model-Based Testing. In the field of testing, two main directions have been investigated for quite a long time. In property-oriented testing (POT) [4, 12], test data is created with the objective to check whether an implementation fulfils or violates a given property which may be specified by Boolean expressions (invariants, pre-/post-conditions) or more complex temporal formulae [12]. In model-based testing (MBT) [19], a reference model expressing the desired behaviour of an implementation is used for generating the test data and for checking the implementation behaviour observed during test executions. In the research community, the objective of MBT is usually to investigate whether an implementation conformed to the model according to some pre-defined equivalence or refinement relation.

In industry, however, testing of cyber-physical systems is usually performed by a hybrid approach, involving both properties and models. Requirements are specified as properties, and models are used as starting points of system and software design [13, 14]. It is checked by review or by model checking that the models reflect the given properties in the correct way. Due to the complexity of large embedded systems like railway and avionic control systems, testing for model conformance only happens on sub-system or even module level, while testing on system integration level or system level is property-based, though models are available. In particular during regression testing, test cases are selected to check specific requirements, and hardly ever to establish full model conformance.

Problem Statement. The objective of this paper is to establish a sufficient black-box test condition for an implementation to satisfy an LTL safety property.¹ Reference models specifying the desired behaviour are represented as symbolic finite state machines (SFSMs) extending finite state machines (FSMs) in Mealy format by input and output variables, guard conditions, and output expressions. Recently, SFSMs have become quite popular in model-based testing (MBT) [16, 18], because they can specify more complex data types than FSMs and can be regarded as a simplified variant of UML/SysML state machines. Also, they are easier to analyse than the more general Kripke structures which have been investigated in model checking [3], as well as in the context of MBT, for example in [7, 8]. In contrast to Kripke structures, SFSMs only allow for a finite state space. This fact can be leveraged in test generation algorithms by enumerating all states and performing more efficient operations on this set of states instead of a potentially infinite one.

The existence of a model in addition to the property to be verified is exploited to guide the test case generation process. Moreover, the model is used as a test oracle which checks more than just the given property: if another violation of the expected implementation behaviour is detected while testing whether the property is fulfilled, this is a “welcome side effect”. This approach deliberately deviates from the “standard approach” to check only for formula violations using, for example, the finite LTL encoding presented in [2] or observers based on some variant of automaton [5].

Main Contributions. The main contributions of this paper are as follows. (1) We present a test case generation procedure which inputs an LTL safety property to be checked and a reference model to guide the generation process and serve as a test oracle. (2) A theorem is presented and explained, stating that test suites generated by this procedure are exhaustive in the sense that every implementation violating the given property will fail at least one test case, provided that the true implementation behaviour is reflected by another SFSM contained in a well-defined fault-domain.² This hypothesis is necessary in black-box testing, because hidden internal states cannot be monitored [17, 21].

To the best of our knowledge, this mixed property-based and model-based approach to POT has not been investigated before outside the field of finite state machines. Only for the latter, strategies for testing simpler properties with additional FSM models have been treated by the authors in [9, 10]. While the approach presented here is related to the one presented in [10], we will elaborate here how to derive test cases for properties on non-deterministic reference models. Furthermore, our approach is distinguished from [9, 10] by operating on SFSMs and by using LTL formulae as the specification formalism for properties. SFSMs are considerably more expressive than FSMs for modelling complex reactive systems. Specifying properties in LTL is more general, intuitive, and elegant than the FSM-specific restricted specification style used in [9, 10].

Overview. In Sect. 2, SFSMs are defined, and existing results about model simulations, equivalence classes, and abstractions to FSMs are reviewed and illustrated by examples. These (mostly well-known) facts are needed to prove the exhaustiveness of the test generation strategy described in Sect. 3. In Sect. 3, fault domains are introduced and a sufficient condition for exhaustive test suites for property verification is presented and proven. For implementing test suite generators, we can refer to algorithms already published elsewhere. Section 4 contains conclusions and sketches future work.

Throughout this paper, we refer to related work where appropriate.

2 Symbolic Finite State Machines, Simulations, Equivalence Classes, and FSM Abstractions

Definition of Symbolic Finite State Machines. A Symbolic Finite State Machine (SFSM) is a tuple $M=(S,s_0,R,V_I,V_O,D,\varSigma _I,\varSigma _O)$. Finite set S denotes the state space, and $s_0\in S$ is the initial state. Finite set $V_I$ contains input variable symbols, and finite set $V_O$ output variable symbols. The sets $V_I$ and $V_O$ must be disjoint. We use V to abbreviate $V_I\cup V_O$. We assume that the variables are typed, and infinite domains like reals or unlimited integers are admissible. Set D denotes the union over all variable type domains. The input alphabet $\varSigma _I$ consists of finitely many guard conditions, each guard being a quantifier-free first-order expression over input variables. The finite output alphabet $\varSigma _O$ consists of output expressions; these are quantifier-free first-order expressions over (optional) input variables and at least one output variable. We admit constants, function symbols, and arithmetic expressions in these expressions but require that they can be solved based on some decision theory, for example, by an SMT solver. Set $R\subseteq S\times \varSigma _I\times \varSigma _O\times S$ denotes the transition relation.

This definition of SFSMs is consistent with the definition of ‘symbolic input/output finite state machines (SIOFSM)’ introduced in [16], but is slightly more general: SIOSFMs allow only assignments on output variables, while our definitions admits general quantifier-free first-order expressions. This is useful for specifying nondeterministic outputs and – of particular importance in this paper – for performing data abstraction, as introduced below. Also, note that [16] only considers conformance testing, but not property-based testing.

Following [16], faulty behaviour of implementations is captured in a finite set of mutant SFSMs whose behaviour may deviate from that of the reference SFSM by (a) faulty or interchanged guard conditions, (b) faulty or interchanged output expressions, (c) transfer faults consisting of additional, lost, or misdirected transitions, and (d) added or lost states (always involving transfer faults as well). To handle mutants and reference model in the same context, we require that (a) the faulty guards are also contained in the input alphabet, and (b) the faulty output expressions are also contained in the output alphabet, (without occurring anywhere in the reference model).

A valuation function $\sigma : V \longrightarrow D$ associates each variable symbol $v\in V$ with a type-conforming value $\sigma (v)$. Given a first-order expression $\phi$ over variable symbols from V, we write $\sigma \,\models \, \phi$ and say that $\sigma$ is a model for $\phi$ if, after replacing every variable symbol v in $\phi$ by its value $\sigma (v)$, the resulting Boolean expression evaluates to true. Only SFSMs that are well-formed are considered in this paper: this means that for every pair $(\phi ,\psi )\in \varSigma _I\times \varSigma _O$ occurring in some transition $(s,\phi ,\psi ,s')\in R$, at least one model $\sigma \,\models \,\phi \wedge \psi$ exists for the conjunction $\phi \wedge \psi$ of guard and output expression. An SFSM with integer variables $x\in V_I$ and $y\in V_O$ and a transition $(s,x< 0, y^2 < x,s')$, for example, would not be well-formed.

Fig. 1.

Simple alarm system M (O = OK, W = warning, A = alarm, $\text {O}< \text {W} < \text {A}$).

Example 1

The SFSM in Fig. 1 describes a simple alarm indication system which inputs a sensor value $x :\mathbb {R}$ and raises an alarm ($y = A$) if x exceeds the threshold value $\max$. After an alarm has been raised, the system remains in state $s_2$ until x drops below the value $\max - \delta$, whereafter a transition to initial state $s_0$ is performed, accompanied by output $y = O$ (“value is OK”). If the threshold value $\max$ has been reached but not yet overstepped, a warning $y = W$ may or may not be issued (nondeterministic decision). If the warning is given, the system transits to state $s_1$ and stays there until $x < \max$ is fulfilled or an alarm needs to be raised because x exceeds the threshold. Output values O, W, A are typed by an enumeration.

Note that in this example, outputs could simply be specified by assignments, so the system could also be modelled as an SIOSFM. Example 4 below shows where the first-order representation is needed.

A symbolic trace of SFSM M is a finite sequence

$$ \tau = (\phi _1/\psi _1)\dots (\phi _n/\psi _n)\in (\varSigma _I\times \varSigma _O)^* $$

satisfying (recall that $s_0$ is the initial state)

$$ \exists s_1,\dots ,s_n\in S: \forall i\in \{1,\dots ,n\}: (s_{i-1},\phi _i,\psi _i,s_i)\in R. $$

This means that there exists a state sequence starting from the initial state, such that each pair $(s_{i-1},s_i)$ of states is linked by a transition labelled with $(\phi _i,\psi _i)$. We use the intuitive notation $(\phi _i/\psi _i)$ inherited from Mealy machines for these predicate pairs, since $\phi _i$ specifies inputs and $\psi _i$ outputs.

A concrete trace (also called computation) of M is a finite sequence of valuation functions

$$ \kappa = \sigma _1\dots \sigma _n \in (V\longrightarrow D)^* $$

such that a symbolic trace $\tau = (\phi _1/\psi _1)\dots (\phi _n/\psi _n)$ of M exists satisfying

$$ (\sigma _1\,\models \,\phi _1\wedge \psi _1)\wedge \dots \wedge (\sigma _n\,\models \,\phi _n\wedge \psi _n). $$

If this condition is fulfilled, $\kappa$ is called a witness of $\tau$. This interpretation of SFSM computations corresponds to the synchronous interpretation of state machine inputs and outputs, as discussed in [20]: inputs and outputs occur simultaneously, that is, in the same computation step $\kappa (i)$.

An SFSM is deterministic if a sequence of input tuples already determines the sequence of associated outputs in a unique way. More formally, two computations $\kappa = \sigma _1\dots \sigma _n$ and $\kappa ' = \sigma _1'\dots \sigma _n'$ satisfying $\sigma _i|_{V_I} = \sigma _i'|_{V_I}$ for all $i=1,\dots ,n$ already fulfil $\kappa = \kappa '$.

As usual in the field of modelling formalisms for reactive systems, the behaviour of an SFSM is defined by the set of its computations. Two SFSMs are equivalent if and only if they have the same set of computations.

Example 2

The alarm system specified in Example 1 has a symbolic trace

$$\begin{aligned} \tau= & {} (x\le \max /y=O).(x\le \max /y=O).\\& (x=\max /y=W).(x>\max /y=A).(x<\max -\delta /y=O) \end{aligned}$$

With constants $\max = 100, \delta =10$, the concrete trace

$$\begin{aligned} \kappa= & {} \{ x\mapsto 100, y \mapsto O\}.\{ x\mapsto 50, y \mapsto O\}. \\& \{ x\mapsto 100, y \mapsto W\}.\{ x\mapsto 110, y \mapsto A\}.\{ x\mapsto 89, y \mapsto O\} \end{aligned}$$

is a witness of $\tau$. The alarm system is nondeterministic, since it also has symbolic trace

$$\begin{aligned} \tau '= & {} (x=\max /y=W).(x\le \max /y=O).\\& (x=\max /y=W).(x>\max /y=A).(x<\max -\delta /y=O) \end{aligned}$$

for which

$$\begin{aligned} \kappa '= & {} \{ x\mapsto 100, y \mapsto W\}.\{ x\mapsto 50, y \mapsto O\}. \\& \{ x\mapsto 100, y \mapsto W\}.\{ x\mapsto 110, y \mapsto A\}.\{ x\mapsto 89, y \mapsto O\} \end{aligned}$$

is a witness. The input sequences of $\kappa$ and $\kappa '$ are identical, but the computations differ.

Testability Assumptions. To ensure testability, the following pragmatic assumptions and restrictions are made. (1) When testing nondeterministic implementations, it may be necessary to apply the input trace several times to reach a specific internal state, since the input trace may nondeterministically reach difference states. As is usual in nondeterministic systems testing, we adopt the complete testing assumption, that there is some known $k\in \mathbb {N}$ such that, if an input sequence is applied k times, then all possible responses are observed [6], and all states reachable by means of this sequence have been visited.

(2) Any two different states of the reference SFSM are reliably distinguishable [6]: if a computation $\kappa$ could nondeterministically reach two different states $s_1$ or $s_2$ of M, then there exists an input sequence that, when applied to the unknown target state reached by $\kappa$, will lead to an output sequence allowing to determine whether the unknown state had been $s_1$ or $s_2$. Note that the alarm system modelled in Fig. 1 is reliably distinguishable for trivial reasons: the target state reached by a computation is already uniquely determined by the sequence of its input/output pairs.

(3) It is required that the output expressions in $\varSigma _O$ are pairwise distinguishable by finitely many input values. This enables us to check the correctness of output expressions with finitely many test cases. Note that this is not a very hard restriction, since for many function classes with infinite domain and image, its members are uniquely determined by a finite number of arguments. For example, linear expressions $\mathtt{y = a\cdot x + b}$ can be pairwise distinguished by two different values of x; and this fact can be generalised to polynomials of a fixed degree in several variables $x_1,\dots ,x_k$. Note that this restriction is vacuous for the alarm system modelled in Fig. 1, since its output expressions do not contain input x.

Property Specifications in LTL. To state behavioural properties of a given SFSM M, we use linear temporal logic LTL [3] with formulae over variable symbols from $V=V_I\cup V_O$. The syntax of LTL formulae $\varphi$ used in this paper is given by grammar

$$\begin{aligned} \varphi&{:}{:}{=}&\phi \ |\ \lnot \varphi \ |\ \varphi \wedge \varphi \ |\ \mathbf {X}\varphi \ |\ \varphi \mathbf {U}\varphi \ |\ \mathbf {F}\varphi \ |\ \mathbf {G}\varphi , \end{aligned}$$

where $\phi$ denotes atomic propositions written as quantifier-free first-order expressions over symbols from V. The semantics of LTL formulae is defined over concrete traces $\kappa$ of M by the following valuation rules.

Here $\kappa ^i$ denotes the trace segment $\kappa (i).\kappa (i+1).\kappa (i+2)\dots$. The semantics of path operators $\mathbf {F}$ and $\mathbf {G}$ is defined via equivalences $\mathbf {F}\varphi \equiv (\text {true}\mathbf {U}\varphi )$ and $\mathbf {G}\varphi \equiv \lnot \mathbf {F}\lnot \varphi$.

Example 3

Consider the property R1. If the value of x never exceeds threshold $\max$, then an alarm will never be raised. This is expressed by LTL formula (recall the ordering $O< W < A$ of output values)

$$ \varPhi _1 \equiv \mathbf {G}(x \le \max ) \Longrightarrow \mathbf {G}(y < A) $$

Simulation Construction. Given an SFSM M, any set of atomic first-order expressions with free variables in V induces a simulation $M^\text {sim}$. Here, this well-known concept is only explained in an intuitive way, for a detailed introduction readers are referred to [3]. It will be shown below how abstracted SFSMs also facilitate property-oriented testing.

Any set of atomic first-order expressions over V can be separated into expressions $f_1,\dots , f_k$ containing free variables from $V_I$ only and expressions $g_1,\dots ,g_\ell$ each containing at least one free variable from $V_O$.

As a first step, this leads to a refinement $M'$ of the model SFSM M by means of the following steps. (1) A transition $(s,\phi ,\psi ,s')$ is replaced by transitions $(s,\phi \wedge \alpha ,\psi \wedge \beta ,s')$, such that each $\alpha$ is conjunction of all $f_1,\dots , f_k$ in positive or negated form, and expression $\beta$ is a conjunction of all $g_1,\dots ,g_\ell$ in positive or negated form. (2) Only the transitions $(s,\phi \wedge \alpha ,\psi \wedge \beta ,s')$ possessing a model $\sigma : V\longrightarrow D$ for $\phi \wedge \alpha \wedge \psi \wedge \beta$ are added in this replacement.

Then a new SFSM $M^\text {sim}$ is created as follows. (1) The states and the initial state of $M^\text {sim}$ are those of M. (2) The transitions of $M^\text {sim}$ are all $(s,\phi \wedge \alpha ,\beta ,s')$, where there exists an output expression $\psi$ such that $(s,\phi \wedge \alpha ,\psi \wedge \beta ,s')$ is a transition of the refined SFSM $M'$.

An SFSM $M^\text {sim}$ constructed according to this recipe is a simulation of $M'$ in the following sense: For every computation $\kappa = \sigma _1\dots \sigma _n$ of $M'$, there exists a symbolic trace $\tau ^\text {sim} = (\phi _1/\psi _1)\dots (\phi _n/\psi _n)$ of $M^\text {sim}$, such that (a) $\kappa$ is witness of $\tau ^\text {sim}$, and (2) any conjunction of positive and negated $f_1,\dots , f_k$ and $g_1,\dots ,g_\ell$ for which $\sigma _i$ is a model is also an implication of $(\phi _i\wedge \psi _i$).

Fig. 2.

Refinement $M'$ of the simple alarm system from Fig. 1 with respect to atomic propositions $x\le \max$ and $y < A$. Here, the ellipses represent the original guard or output condition, respectively. The transition from s1 to s0 shows an actual example.

Example 4

From property $\varPhi _1 \equiv \mathbf {G}(x \le \max ) \Longrightarrow \mathbf {G}(y < A)$ discussed in Example 3 the atomic propositions $f \equiv (x\le \max )$ and $g\equiv (y<A)$ are extracted. The rules for creating a refined machine result in the machine shown in Fig. 2.

Applying the construction rules for the SFSM abstracted from the alarm system with respect to $f,g,\lnot f,\lnot g$ results in the machine shown in Fig. 3. As an example of a concrete trace of the alarm system, we take again

$$\begin{aligned} \kappa= & {} \{ x\mapsto 100, y \mapsto O\}.\{ x\mapsto 50, y \mapsto O\}. \\& \{ x\mapsto 100, y \mapsto W\}.\{ x\mapsto 110, y \mapsto A\}.\{ x\mapsto 89, y \mapsto O\} \end{aligned}$$

This is a witness of the symbolic trace (we omit the other conjuncts besides $x\le max$ and its negation)

$$\begin{aligned} \tau ^\text {sim}= & {} (\dots \wedge x \le \max /y< A).(\dots \wedge x \le \max /y< A).(\dots \wedge x \le \max /y< A).\\& (\dots \wedge \lnot (x \le \max )/\lnot (y< A)).(\dots \wedge x \le \max /y < A) \end{aligned}$$

of the abstracted SFSM.

Fig. 3.

Simulation $M^\text {sim}$ of the simple alarm system from Fig. 1 with respect to atomic propositions $x\le \max$ and $y < A$.

Input Equivalence Classes and FSM Abstraction. In [7, 8] we have presented a testing theory allowing to abstract a variant of Kripke structures to FSMs by means of an input equivalence class construction. The SFSMs considered in this paper can be interpreted as Kripke structures of this variant. The main result of this theory is that test suites generated for the abstracted FSMs can be translated back to the concrete Kripke model level while preserving the test strength of the original FSM-based suite. While the method proposed in this paper could also be formulated in this more general framework of Kripke structures being used as models and abstracted to FSMs, we decided to present it using SFSMs and abstract these to FSMs. This allows for a simpler description of the abstraction process and implies restrictions that would have to be mentioned explicitly and accounted for in the context of Kripke structures. These restrictions guarantee the existence of an FSM abstraction of the model.

We apply the test strength-preserving translation technique from FSM test cases to concrete Kripke test cases in Sect. 3 to prove that the test strategy introduced there is exhaustive in the sense that it will uncover every property violation of the SUT, provided that certain hypotheses are fulfilled. Therefore, the main facts of the testing theory elaborated in [7, 8] are summarised in the following paragraphs.

The theory applies to systems with arbitrary (possibly infinite) input domains and finite domains for internal state variables and output variables. Since our SFSMs are allowed to work with infinite output domains, it is first necessary to create an abstraction with finite output domains.

Step 1. The refined reference model $M'$ constructed above with the atomic propositions of the LTL formula under consideration is further refined by creating input equivalence classes. The classes are constructed by building all conjunctions of positive and negated guard conditions contained in the input alphabet. As before, expressions without a model are dropped. Recall that the input alphabet also contains the possible faulty guards. This further refinement of $M'$ is denoted by $M_c'$.

The effect of this construction is as follows. A symbolic input sequence $\iota = \phi _1\dots \phi _k$ consisting of quantifier-free first-order input class expressions $\phi _i$ refining the original guards of $M'$ determines finitely many possible symbolic traces in the reference model $M_c'$ and in any possible SFSM over the same alphabet, specifying the true behaviour of a (correct or faulty) implementation. In the deterministic case, this symbolic trace is already uniquely determined by $\iota$.

Step 2. From each refined input class, sufficiently many inputs are selected so that the output expressions that are expected when applying an input from this class in any state can be distinguished from any other output expression contained in $\varSigma _O$ which would be faulty for inputs from this class.

Note that is some situations, an input class X is so small that the distinction between all output expressions is no longer possible. In this case, however, different output expressions would be admissible for the implementation, if their restrictions to X coincide. For example, if X only contains the input value $x = 0$, and $\varSigma _O = \{ \mathtt{y = 3}, \mathtt{y = 0}, \mathtt{y = 3\cdot x} \}$, then output expressions $\mathtt{y = 0}$ and $\mathtt{y = 3\cdot x}$ are indistinguishable on X. If output $y = 0$ is expected for input $x=0$ in the given state, then both expressions would be acceptable in an implementation. The concrete input selections are represented again as valuation functions $s_x : V_I \longrightarrow D$.

The collected concrete inputs $s_x$ selected from the input classes are used to define the (finite) input alphabet $A_I$ of the FSM abstraction constructed by means of the recipe introduced here.

Step 3. Applying the finite number of inputs from each class to every possible output expression associated with this class yields a finite number of values from the possibly infinite output domain. These values are written as valuation functions $s_y : V_O \longrightarrow D$ and used as the output alphabet $A_O$ of the FSM under construction.

Step 4. The state space and initial state of the FSM is identical to the states of $M'$.

Step 5. The transition relation of the FSM is defined by including $(s,s_x,s_y,s')$ in the relation if and only if there exists a transition $(s,\phi ,\psi ,s')$ in $M_c'$ such that $s_x\in A_I \wedge s_y \in A_O\wedge (s_x \cup s_y) \,\models \, \phi \wedge \psi$.

The observable, minimised FSM abstraction constructed in these 5 steps is denoted as $F(M_c')$. The construction recipe above is illustrated in the following example.

Example 5

For the refined alarm system $M'$ shown in Fig. 2, let us assume that the possibly faulty implementations may only mix up guard conditions, but do not mutate them. Then the input equivalence classes calculated according to the recipe described above are listed in the following table. Recall that the constants have been fixed as $\delta = 10, \ \max = 100$.

Since the output expressions do not refer to input variable x, a single representative from each input class can be chosen to create the FSM abstraction: the output expressions of $M_c'$ can always be distinguished by their concrete values.

Class	Specified by	Concrete input $s_x$ for $A_I$
$c_0$	$x < \max -\delta$	$\{x \mapsto 50 \}$
$c_1$	$\max -\delta \le x <\max$	$\{x \mapsto 95 \}$
$c_2$	$x = \max$	$\{x \mapsto 100 \}$
$c_3$	$\max < x$	$\{x \mapsto 110 \}$

Fig. 4.

Alarm system refinement $M'_c$ resulting from application of input equivalence classes to $M'$ from Fig. 2. For brevity, we have consolidated multiple transitions back into one for this figure, if the beginning and end states of these were the same as well as their output condition. This is signified by commas in their input condition, separating the input conditions of individual transitions.

The SFSM $M'_c$ further refining $M'$ by means of these input classes is shown in Fig. 4. We use a short-hand notation where one transition arrow can be labelled by several guards if the output expression is the same in each transition. The abstraction FSM $F(M_c')$ constructed according to the five steps described above is shown in Fig. 4.

Fig. 5.

Finite state machine $F(M_c')$ abstracting the SFSM $M_c'$ from Fig. 4. Input valuations $\{x\mapsto \text {value}\}$ are abbreviated by ‘$\text {value}$’, output valuations $\{y\mapsto \text {value}\}$ by ‘$\text {value}$’.

The simulation $M^\text {sim}$ of the alarm system is also refined by the same input equivalence classes. This results in the SFSM shown in Fig. 6. For this SFSM’s abstracting FSM, we define output symbols

Symbol	Output expression
$e_0$	$y<A$
$e_1$	$\lnot (y<A)$

Then we use the same concrete input alphabet as for $F(M_c')$. The resulting FSM is shown in Fig. 7.

After having made this FSM observable and minimal, the resulting prime machine $F(M^\text {sim}_c)$ has the structure shown in Fig. 8.

Admissible Simulations. To specify precisely which types of simulations $M^\text {sim}_c$are admissible, we introduce the concept of output abstractions for FSMs. Let $\omega : A_O \longrightarrow A_O'$ be a function between output alphabets. Then any FSM $F = (S,s_0,T,A_I,A_O)$ with alphabet $(A_I,A_O)$, state space S, initial state $s_0$, and transition relation $T\subseteq S\times A_I\times A_O \times S$ can be mapped to an FSM $\omega (F)$ which is constructed by creating FSM $(S,s_0,T',A_I,A_O')$ over alphabet $(A_I,A_O')$ and transition relation

$$ T' = \{ (s,a,\omega (b),s')~|~(s,a,b,s')\in T \}, $$

and constructing the prime machine (i.e. the observable and reduced FSM) of $(S,s_0,T',A_I,A_O')$. The FSM $F'$ is called the output abstraction of F with respect to $\omega$. The mapping $\omega$ is called state-preserving for F, if $\omega (F)$ maps traces leading to the same state in F to traces leading to the same state in $\omega (F)$ as well.

It is easy to see that the prime machine $F(M^\text {sim}_c)$ shown in Fig. 8 has been created from $F(M_c')$ in Fig. 5 by means of the output abstraction $\omega = \{ O \mapsto e_0, W \mapsto e_0, A \mapsto e_1 \}$. Comparison of $F(M_c')$ in Fig. 5 and Fig. 8 shows that this $\omega$ is state-preserving.

For deterministic FSMs, every output abstraction is state-preserving, but this is not always the case for nondeterministic FSMs. The exhaustive test suite generation procedure for property checking introduced in the next section requires that simulations are constructed by means of state-preserving output abstractions.

Fig. 6.

Alarm system simulation $M^\text {sim}_c$ from Fig. 3 – further refined by input equivalence classes.

3 An Exhaustive Property-Based Testing Strategy

Prerequisites. Throughout this section, $M = (S,s_0,R,V_I,V_O,D,\varSigma _I,\varSigma _O)$ denotes an SFSM reference model specifying the required behaviour of some implementation whose true behaviour is represented by some (possibly non-equivalent) SFSM I, defined over the same alphabet, as explained in Sect. 2. Set P denotes a finite set of atomic quantifier-free first-order expressions with free variables in V. The properties to be tested are all contained in the set of LTL formulae over atomic expressions from P. As introduced in Sect. 2, the SFSM $M_c'$ has been created from M by refining the guards and the output expressions according to the atomic expressions in P and the input equivalence classes induced by $\varSigma _I$. The FSM associated with $M_c'$ is denoted by $F(M_c')$. It is assumed that $F(M_c')$ is a prime machine; this means that it is an observable and minimal FSM [15]. We assume that $F(M_c')$ has $n > 1$ states.³ The simulation SFSM $M^\text {sim}_c$ has the same input alphabet as $M_c'$, but a (usually smaller) output alphabet containing output expressions of P only. The prime machine associated with $M^\text {sim}_c$ is denoted by $F(M^\text {sim}_c)$. The input alphabet of $F(M_c')$ and $F(M^\text {sim}_c)$ (i.e. the concrete valuations selected from each input class) is denoted by $A_I$, the output alphabet of $F(M_c')$ by $A_O$, and that of $F(M^\text {sim}_c)$ by $A_O^\text {sim}$.

Fig. 7.

Finite state machine abstracting the SFSM $M^\text {sim}_c$ from Fig. 6.

Fig. 8.

Prime machine $F(M^\text {sim}_c)$ (observable, minimised FSM constructed from the FSM in Fig. 7).

Fault Domains. In black-box testing, fault domains⁴ are introduced to constrain the possibilities of faulty behaviours of implementations. Without these constraints, it is impossible to guarantee exhaustiveness with finite test suites: the existence of hidden internal states leading to faulty behaviour after a trace that is longer than the ones considered in a finite test suite cannot be checked in black-box testing. In the context of this paper, a fault domain is a set of SFSMs, always containing the reference model (usually in refined form) representing the intended behaviour. It is assumed that the implementation’s true behaviour is reflected by one of the SFSM models in the fault domain.

Now the fault domain $\mathcal{D}(M_c',m)$ contains all SFSMs possessing the same input alphabet and output alphabet as $M_c'$, such that their abstractions to prime machines constructed in analogy to $F(M_c')$ do not have more than m states.

Property-Related Exhaustiveness. Given the set P of quantifier-free atomic first-order expressions over variables from V, a test suite is P-exhaustive for a given fault domain $\mathcal{D}(M_c',m)$, if every SFSM I representing an implementation behaviour fails at least one test whenever I contains a computation $\kappa _I$ that is not a witness for any symbolic trace of $M^\text {sim}_c$.

Example 6

Consider again the alarm system M from Fig. 1 and the property $\varPhi _1 \equiv \mathbf {G}(x \le \max ) \Longrightarrow \mathbf {G}(y < A)$. Then, with the guard refinements introduced for $M'_c$ and $M^\text {sim}_c$, the atomic expressions to consider are

$$ P=\{x< \max -\delta , \max -\delta \le x<\max , x=\max , y<A\}. $$

Expressed in terms of P-elements, property $\varPhi _1$ can be equivalently expressed as

$$ \varPhi _1 \equiv \mathbf {G}(x< \max -\delta \vee \max -\delta \le x<\max \vee x=\max ) \Longrightarrow \mathbf {G}(y < A). $$

Now consider an implementation whose behaviour I differs from that of M only by the mutated guard in the transition from $s_0 \longrightarrow s_2$, where we assume that I’s guard is $x\ge \max$ instead of $x>\max$, as specified in M. With this guard mutation as the only fault, I is in the fault domain $\mathcal{D}(M_c',m)$ of the alarm system M. Then, for example, I has a computation (it is assumed again that $\max =100$ and $\delta =10$)

$$ \kappa _I = \{ x\mapsto 50, y\mapsto O \}.\{ x\mapsto 100, y\mapsto A \}. $$

Abstracted to a symbolic trace over P, this results in

$$ \tau _I = (x< \max -\delta /y<A).(x=\max /\lnot (y<A)). $$

Obviously, this is not a symbolic trace of $M^\text {sim}_c$, as depicted in Fig. 6. Therefore, any P-exhaustive test suite should fail for I.

Test Suite Generation Procedure. In preparation of the test generation, SFSMs $M_c'$ and $M^\text {sim}_c$ are created for the given set of P of quantifier-free atomic first-order expressions over variables from V, as explained in Sect. 2. Then their FSM abstractions are constructed (also according to the recipe explained in Sect. 2), and their prime machines are constructed, as described in [15], resulting in FSMs $F(M_c')$ and $F(M^\text {sim}_c)$, respectively. It is required that $F(M^\text {sim}_c)$ has been created from $F(M_c')$ by means of a state-preserving output abstraction.

The rationale behind deriving these FSMs is as follows. FSM $F(M_c')$ contains sufficiently detailed information to derive tests suitable for detecting any violation of observational equivalence. While the proof for this fact is quite technical, it is fairly intuitive to understand: By construction, $F(M_c')$ uses concrete input values from every input equivalence class of any implementation whose true behaviour is reflected by an SFSM I in the fault domain $\mathcal{D}(M_c',m)$. It is possible to derive a collection of input sequences from $F(M_c')$, so that every input class of I is exercised from every state of I. To ensure this, the assumption that I’s FSM abstraction does not have more than m states is essential. Moreover, the input alphabet of $F(M_c')$ has been constructed in such a way that sufficiently many values of each input class are exercised on the implementation, such that every output expression error will be revealed.

Next, we realise that testing for observational equivalence is actually more than we really need. So we wish to relax the test requirements in such a way that the test focus is to check whether the satisfaction for atomic properties from P along any computation of I conforms to that of $M'_c$. For this purpose, $F(M^\text {sim}_c)$ is needed. Typically, $F(M^\text {sim}_c)$ has fewer states than $F(M_c')$ and I. Therefore, we cannot completely forget about $F(M_c')$, because this machine influences the length of the traces used to test I. If tests were constructed from $F(M^\text {sim}_c)$, we would either use traces of insufficient length or use too many traces of adequate length, since $F(M^\text {sim}_c)$ does not provide any information about which traces of maximal length are relevant.

These intuitive considerations lead to the test suite generation procedure described next.

We create an FSM test suite $H_P^\text {fsm}$ from $F(M_c')$ and $F(M^\text {sim}_c)$ as follows. Let $V\subseteq \varSigma _I^*$ be a minimal state cover of $F(M_c')$ containing the empty trace $\varepsilon$. A state cover is a set of input traces, such that for each state s of $M_c'$, there exists a trace from V reaching s. Define auxiliary sets ($A_I^i$ denotes the set of FSM input traces of length i).

$$ A = V\times V \qquad B = V\times \big (V.\bigcup _{i=1}^{m-n+1}A_I^{i}\big ) $$

$$\begin{aligned} C= & {} \{(\nu .\gamma ', \nu .\gamma )~|~\nu \in V \wedge \gamma \in \big (\bigcup _{i=1}^{m-n+1}A_I^{i}\big ) \wedge \gamma '\in \text {Pref}(\gamma )-\{\varepsilon \}\} \end{aligned}$$

Then define a set D of input trace pairs such that D contains (a) all trace pairs from A leading to different states in the FSM state space of $F(M_c')$, (b) every trace pair of B and C leading to different states in $F(M^\text {sim}_c)$ (note that states distinguishable in $F(M_c')$ may not be distinguishable anymore in $F(M^\text {sim}_c)$, but state pairs distinguishable in $F(M^\text {sim}_c)$ are always distinguishable in $F(M_c')$).

Let function $\varDelta : D \longrightarrow A_I^*$ map trace pairs $(\alpha ,\beta )$ leading to distinguishable states $(s_1,s_2)$ to input traces $\gamma$ distinguishing $(s_1,s_2)$. Now define test FSM test suite $H_P^\text {fsm}$ by removing all true prefixes from the test case set

$$ V.A_I^{m-n+1}\cup \{ \alpha .\varDelta (\alpha ,\beta ), \beta .\varDelta (\alpha ,\beta )~|~(\alpha ,\beta )\in D\}. $$

Since the input traces in $H_P^\text {fsm}$ are already sequences of concrete values (recall that the input alphabet of $F(M_c')$ consists of concrete values taken from input equivalence classes), we can use them directly as test cases, to be executed against the system under test.

Proving P-Exhaustiveness. The following Lemma shows that $M^\text {sim}_c$ is crucial for deciding whether an implementation satisfies an LTL formula over atomic expressions from P. It follows directly from the construction rules for $M^\text {sim}_c$ in Sect. 2.

Lemma 1

Suppose that the true behaviour of an implementation is given by SFSM $I\in \mathcal{D}(M_c',m)$. Suppose further that every computation of I is also a witness of a symbolic trace in $M^\text {sim}_c$. Then I satisfies every LTL formula over positive and negated atomic first-order expressions from P which is satisfied by the reference SFSM M.

The following main theorem states the exhaustiveness of the test suite generation procedure described above.

Theorem 1

The test suite $H_P$ constructed above is P-exhaustive for all implementations whose true behaviour is specified by one of the SFSMs contained in the fault domain $\mathcal{D}(M_c',m)$ specified above.

The proof of the theorem is performed along the following lines.⁵ In a first step, the exhaustiveness of the FSM test suite which is created as part of the generation procedure is proven. This is quite similar to the proof presented in [10, Theorem 2], but operates here with a different FSM abstraction $F(M^\text {sim}_c)$ that may also be nondeterministic. It is essential for this proof that simulations have been generated by means of state-preserving output abstractions.

A second step shows that the selection of concrete input values from input equivalence classes described in the previous section is adequate to uncover every deviation of the implementation behaviour from the specified behaviour. For the proof of this theorem, it is essential that all possible guard mutations and output expression mutations are already contained in the input and output alphabets, respectively. Moreover, it is exploited that sufficiently many concrete values have been selected from the input classes to distinguish faulty output expressions from correct ones.

In practice, it often cannot be decided whether an implementation regarded as a black-box is represented by an SFSM I inside $\mathcal{D}(M_c',m)$ or not. For guaranteed exhaustiveness, a grey-box approach performing preliminary static analyses on the implementation code would be required in order to prove that I is inside the fault domain. If this cannot be achieved, it is reassuring to know that test suites constructed according to the generation procedure above have significantly higher test strength than naive random testing, even if I lies outside the fault domain. This has been evaluated in [11].

4 Conclusion

In this paper, an exhaustive test suite for testing LTL properties has been presented. It is based on both a symbolic finite state machine model describing the expected behaviour and the formula. By using simulation and abstraction techniques, a test suite generation procedure has been presented which guarantees to uncover every property violation, while possibly finding additional violations of observational equivalence, provided that the implementation’s true behaviour is captured by an element of the fault domain. The simulations and abstractions used frequently allow for test suites that are significantly smaller than those testing for equivalence between model and implementation. For a specific variant of properties which is less expressive than LTL, this has already been shown in [10]. We expect similar reductions for the full LTL property checking described here. This will be investigated in the near future, where we will implement the method proposed here as well as improvements upon it in the libfsmtest [1] software library.