# Generating Checking Sequences for User Defined Fault Models

Alexandre Petrenko, Adenilso Simao

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

## To cite this version:

Alexandre Petrenko, Adenilso Simao. Generating Checking Sequences for User Defined Fault Models. 29th IFIP International Conference on Testing Software and Systems (ICTSS), Oct 2017, St. Petersburg, Russia. pp.320-325, 10.1007/978-3-319-67549-7_20. hal-01678955

HAL Id: hal-01678955

https://inria.hal.science/hal-01678955

Submitted on 9 Jan 2018

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
# Generating Checking Sequences for User Defined Fault Models

Alexandre Petrenko

CRIM, Centre de recherche informatique de Montréal
405 Ogilvy Avenue, Suite 101, Montréal (Québec) H3N 1M3, Canada
petrenko@crim.ca

Adenilso Simao

Instituto de Ciencias Matematicas e de Computacao, Universidade de Sao Paulo
Sao Carlos/Sao Paulo, Brazil
adenilso@icmc.usp.br

**Abstract.** In this paper, we investigate how a checking sequence can be generated from a Finite State Machine, with respect to a user-defined set of faults, modeled as a nondeterministic FSM, called Mutation Machine (MM). We propose an algorithm for generating a checking sequence in this scenario and demonstrate its correctness.

**Keywords.** FSM testing, fault models, checking sequence, mutation machine

## 1 Introduction

Generation of checking sequence (CS) from a Finite State Machine (FSM) is a relevant problem, when the implementation may not be reset or when reset operation it prohibitively costly. There are methods which, given a distinguishing sequence, can generate a checking sequence in polynomial time [2] [3]. Other methods generate checking sequence from characterization sets instead of a distinguishing sequence [1], since the former is available for any minimal machine, while the latter may not exist. Those methods, however, rely on the repetition of the sequences in the characterization sets, resulting in an exponentially long sequence. These methods also consider the classical fault domain where the implementation may have arbitrary faults, except extra states.

In this paper, we investigate how a CS can be generated from an FSM, with respect to a subset of faults. The faults of interest are modeled as a nondeterministic FSM, called Mutation Machine (MM), such that any implementation is assumed to be a deterministic submachine of the MM. We propose an algorithm for generating a CS in this scenario. After demonstrating the correctness of the algorithm, we illustrate its application on a simple example.
## 2 Checking Sequence Construction

An FSM is a tuple $M = (S, S_0, X, O, h)$, where $S$ is the set of states, $S_0 \subseteq S$ is the set of initial states, $X$ is the set of inputs, $O$ is the set of outputs, which satisfy the condition $I \cap O = \emptyset$, and $h \subseteq (S \times X \times O \times S)$ is the set of transitions. For state $s$ and input $x$, let $h(s, x)$ be the set of transitions from state $s$ with input $x$. The FSM $M$ is initialized if $|S_0| = 1$ and is deterministic if for each $(s, x) \in S \times X$, $|h(s, x)| \le 1$. For an initialized FSM, where $|S_0| = 1$, write $s_0$, instead of $\{s_0\}$.

The machine $M$ is completely specified (complete FSM) if $|h(s, x)| \ge 1$ for each $(s, x) \in S \times X$; otherwise, it is partially specified (partial FSM).

A path of the FSM $M = (S, S_0, X, O, h)$ from state $s \in S$ is a sequence of transitions $(s_1, x_1, o_1, s_2) (s_2, x_2, o_2, s_3) \dots (s_k, x_k, o_k, s_{k+1})$, such that $(s_i, x_i, o_i, s_{i+1}) \in h$, for $1 \le i \le k$. Notice that we also allow a path to be empty, represented by $\varepsilon$. The machine is strongly connected, if it has a path from each state to any other state. The input projection (output projection) of the path is $x_1x_2\dots x_k (o_1o_2\dots o_k)$. Input sequence $\beta \in I^*$ is a defined input sequence in state $s$ of $M$ if it is an input projection of a path from state $s$. We use $\Omega(s)$ to denote the set of all input sequences defined in state $s$ and $\Omega(M)$ for the states in $S_0$, i.e., for $M$. $\Omega(M) = X^*$ holds for any complete machine $M$, while for a partial FSM $\Omega(M) \subset X^*$.

Given a path $p$, let $\text{trav}(p)$ be the set of transitions of $M$ which appear in $p$. For state $s$ and input $x$, let $\text{trans}(p, (s, x))$ be the set of transitions from state $s$ with input $x$ in $\text{trav}(p)$, i.e., $\text{trans}(p, (s, x)) = \text{trav}(p) \cap h(s, x)$. For the FSM $M = (S, S_0, X, O, h)$, given a set of states $S' \subseteq S$ and an input sequence $\alpha$, let $\text{path}(S', \alpha)$ be the set of paths of $M$ from states of $S'$ with input projection $\alpha$. We denote $\text{path}(S_0, \alpha)$ by $\text{path}_M(\alpha)$. Let $\lambda(S', \alpha)$ be the set of output projections of the paths in $\text{path}(S', \alpha)$; we denote $\lambda(S_0, \alpha)$ by $\lambda_M(\alpha)$. Unless stated otherwise, paths are assumed to be from an initial state.

Given states $s$, $t \in S$ of the deterministic FSM $M = (S, S_0, X, O, h)$, $t$ is quasi-equivalent to $s$, if $\Omega(t) \supseteq \Omega(s)$ and $\lambda(t, \alpha) = \lambda(s, \alpha)$ for all $\alpha \in \Omega(s)$; moreover, in case $\Omega(t) = \Omega(s)$, states are equivalent. States $s$, $t \in S$ are distinguishable, if $\lambda(t, \alpha) \neq \lambda(s, \alpha)$ for some $\alpha \in \Omega(t) \cap \Omega(s)$. The machine is reduced, if any two states are distinguishable. The quasi-equivalence (equivalence) of two deterministic FSMs is the corresponding relation of their initial states.

Spec = (S, s₀, X, O, h) is an initialized deterministic FSM specification. We assume that it is strongly-connected machine, not necessarily complete and reduced.

Given an FSM $M = (S, s_0, X, O, h)$ and $s \in S$, let $M/s$ be the FSM $(S, s, X, O, h)$, i.e., $M$ initialized in state $s$. We let $s$-after-$\alpha$ denote the set of states reached by input sequence $\alpha$ from state $s$; if $\alpha$ is applied to the initial state of $M$ then we write $M$-after-$\alpha$ instead of $s_0$-after-$\alpha$; for deterministic machines, we write $s$-after-$\alpha = s'$ instead of $s$-after-$\alpha = \{s'\}$

We use a so-called *mutation machine* $MM = (S', S'_0, X, O, h')$ which is a completely specified possibly nondeterministic FSM.

FSM $M = (S, s_0, X, O, h)$ is a *submachine* of $MM = (S', S'_0, X, O, h')$ iff $S \subseteq S'$, $s_0 \in S'_0$ and $h \subseteq h'$. Any complete deterministic submachine of $MM$ is one of the *mutants* of *Spec*. The number of mutants is $|S'_0| \prod_{(s, x) \in S \times X} |h'(s, x)|$. For the sets of states $S$,
inputs X and outputs O, we define the machine $\mathit{Chaos}(S, X, O) = (S, s_0, X, O, (S \times X \times O \times S))$ representing the universe of all FSMs with $|S|$ states.

Let $\mathit{Prod}$ be the product of $\mathit{Spec}$ and $\mathit{MM} = (S', S'_0, X, O, h')$; the states of $\mathit{Prod}$ is a subset of $(S \cup \{\Delta\}) \times S'$. A state $(\Delta, s)$ is a $\Delta$-state. The product $\mathit{Prod} = (P, P_0, X, O, H)$, where $P_0 = \{(s_0, s') | s' \in S'_0\}$ is such that $P$ and $H$ are the smallest sets satisfying the following rules:

1. If $(s, s') \in P, (s, x, o, t) \in h, (s', x, o', t') \in h', \text{ and } o = o', \text{ then } (t, t') \in P \text{ and } ((s, s'), x, o, (t, t')) \in H$.

2. If $(s, s') \in P, (s, x, o, t) \in h, (s', x, o', t') \in h', \text{ and } o \neq o', \text{ then } (\Delta, t') \in P \text{ and } ((s, s'), x, o', (\Delta, t')) \in H$.

Notice that $\Delta$-states are sink states. If the product has no $\Delta$-states, then any mutant of $\mathit{MM}$ is quasi-equivalent to $\mathit{Spec}$.

An input sequence $\omega \in \Omega(\mathit{Spec})$ is a checking sequence for $\mathit{Spec}$ w.r.t. $\mathit{MM}$, if for each deterministic submachine $N$ of $\mathit{MM}$, if $\lambda_{\mathit{N}}(\omega) = \lambda_{\mathit{Spec}}(\omega)$, then $N$ is quasi-equivalent to $\mathit{Spec}/s$, where $s \in S$.

Given a path $p = ((s_1, m_1), x_1, o_1, (s_2, m_2)) ((s_2, m_2), x_2, o_2, (s_3, m_3)) \dots ((s_k, m_k), x_k, o_k, (s_{k+1}, m_{k+1}))$ of the product $\mathit{Prod}$ of $\mathit{Spec}$ and $\mathit{MM}$, let $p_{\downarrow MM}$ be the corresponding path in $\mathit{MM}$, i.e., $p_{\downarrow MM} = (m_1, x_1, o_1, m_2) (m_2, x_2, o_2, m_3) \dots (m_k, x_k, o_k, m_{k+1})$.

A path of the product $\mathit{Prod}$ is deterministic (w.r.t. $\mathit{MM}$) if for every state $s$ and input $x$, $|\mathit{trans}(p_{\downarrow MM}, (s, x))| \le 1$. Given a set of paths $Q$ of $\mathit{Prod}$, let $\mathit{det}(Q)$ be the set of paths of $Q$ which are deterministic (w.r.t. $\mathit{MM}$) and $\Delta(Q)$ be the set of deterministic paths which leads to a $\Delta$-state.

**Algorithm for generating a CS for Spec w.r.t. MM**

**Input:** *Spec* and *MM*

**Output:** A CS for *Spec* w.r.t. *MM*

$\omega := \varepsilon$

Compute the product $\mathit{Prod}$ of $\mathit{Spec}$ and $\mathit{MM}$.

**While** there exists a nonempty shortest input sequence $\alpha$, such that
$\Delta(\mathit{det}(\mathit{path}_{MM}(\omega\alpha))) \neq \emptyset$ **do**

$\omega := \omega\alpha$

**End While**

**Return** $\omega$

**Lemma 1.** Let $\omega$ be an input sequence such that for each input sequence $\alpha$, we have that $\Delta(\mathit{det}(\mathit{path}_{MM}(\omega\alpha))) = \emptyset$. Then, $\omega$ is a checking sequence for $\mathit{Spec}$ w.r.t. $\mathit{MM}$.

**Proof.** Assume that $\omega$ is not a checking sequence for $\mathit{Spec}$ w.r.t. $\mathit{MM}$, but for each input sequence $\alpha$, we have that $\Delta(\mathit{det}(\mathit{path}_{MM}(\omega\alpha))) = \emptyset$.

Thus, there exists a deterministic submachine $N$ of $\mathit{MM}$, such that $\lambda_{\mathit{N}}(\omega) = \lambda_{\mathit{Spec}}(\omega)$, and for each $s \in S$, we have that $N$ is not quasi-equivalent to $\mathit{Spec}/s$. This implies that state $N$-after-$\omega$ is not quasi-equivalent to any state $\mathit{Spec}/s$-after-$\omega$. Then for each $s \in S$, there exists an input sequence $\beta \in \Omega(s)$ such that $\lambda_{\mathit{N}/N$-after-$\omega$}(\beta) \neq \lambda_{\mathit{Spec}/s$-after-$\omega$}(\beta)$.
Let $p_{\omega\beta}$ be the path in $N$ which has $\omega\beta$ as the input projection. It follows that $p_{\omega\beta} \in \Delta(\det(\text{path}_{MM}(\omega\beta)))$, since $N$ is deterministic; moreover, it leads to a $\Delta$-state, since $\lambda_{NN\text{-after-}\omega}(\beta) \neq \lambda_{\text{Spec/s-after-}\omega}(\beta)$, thus, $\Delta(\det(\text{path}_{MM}(\omega\beta))) \neq \emptyset$, a contradiction. $\square$

Thus, by Lemma 1, if the algorithm stops, the resulting sequence $\omega$ is indeed a checking sequence. It remains to show that it will always stop for any specification and mutation machine.

**Lemma 2.** After a finite number of steps, the algorithm terminates.

**Proof.** First, notice that for a given deterministic submachine of $MM$, there is exactly one deterministic path with a given input sequence projection (many submachines can share the same path). Thus, the number of paths in $\det(\text{path}_{MM}(\omega))$ is limited by the number of deterministic submachines of $MM$; as there are finitely many such submachines, there are finitely many paths in $\det(\text{path}_{MM}(\omega))$. Let $\text{Sub}_{\omega}$ be the set of deterministic submachines for which correspond the paths in $\det(\text{path}_{MM}(\omega))$. At least one path in $\det(\text{path}_{MM}(\omega))$ leads to a $\Delta$-state, since the algorithm updated $\omega$ in the previous iteration to $\omega\alpha$ and $\Delta(\det(\text{path}_{MM}(\omega\alpha))) \neq \emptyset$.

Let $\alpha$ be a nonempty input sequence, such that $\Delta(\det(\text{path}_{MM}(\omega\alpha))) \neq \emptyset$. Let $\text{Sub}_{\omega\alpha}$ be the set of deterministic submachines each which has a path in $\det(\text{path}_{MM}(\omega\alpha))$. As $\Delta$-states are sink states, any submachine in $\text{Sub}_{\omega}$ with a path to a $\Delta$-state is not in $\text{Sub}_{\omega\alpha}$. Thus, there exists at least one submachine which is in $\text{Sub}_{\omega}$ but not in $\text{Sub}_{\omega\alpha}$. The set of submachines with paths in $\det(\text{path}_{MM}(\omega))$ is thus reduced each time $\omega$ is updated by the algorithm. As the set of submachines is finite, eventually after a finite number of steps the set $\text{Sub}_{\omega}$ has no more machines distinguishable from the specification machine *Spec*, which means that for any input sequence $\alpha$, it holds that $\Delta(\det(\text{path}_{MM}(\omega\alpha))) = \emptyset$, and the algorithm terminates. $\square$

We now illustrate the application of the algorithm. Consider the FSM in Figure 1a. Observe first that it has no distinguishing sequence. In Figure 1b, we include a mutation machine for which we will generate a checking sequence.

<figure><img src="image_3.png" /><figcaption>Figure 1. (a) Specification FSM. (b) the Mutation Machine *MM*</figcaption></figure>

Notice that there are twelve deterministic complete submachines of $MM$. One possibility to obtain a checking sequence for *Spec* is to use any of the applicable methods [2] [3], ignoring *MM*. However, the resulting checking sequence would be unnecessarily long.

The algorithm starts by building the product of *Spec* and *MM*, as well as initializing $\omega$ with the empty sequence. The nonempty input sequence $\alpha = aa$ is such that $\omega\alpha$ reaches a $\Delta$-state in the product, since $\det(\text{path}_{MM}(\omega\alpha)) = \{(1, a, 0, 2), (2, a, 1, 3)), ((1, a, 0, 2), (2, a, 0, \Delta)), ((1, a, 0, 2), (2, a, 1, 2))\}$, i.e., $\Delta(\det(\text{path}_{MM}(\omega\alpha))) \neq \emptyset$. We
<figure><img src="image_4.png" /><figcaption>**Figure 2.** Variation of the Length of the Checking Sequence with respect to the Number of Transitions in the Mutation Machine.</figcaption></figure>

# 4 Conclusion

In this paper, we proposed an algorithm for generating a checking sequence with respect to a user-defined fault model. In the forthcoming steps of this research, we plan to characterize scenarios when the algorithm can be effectively applied as well as its scalability.

# Acknowledgement.

This work was partially supported by MESI (Ministère de l'Économie, Science et Innovation) of Gouvernement du Québec and NSERC of Canada, and by Brazilian Funding Agency FAPESP, Grant 2013/07375-0.

# References

1. Ali Rezaki, Hasan Ural: Construction of checking sequences based on characterization sets. Computer Communications 18(12): 911-920 (1995).

2. Adenilso da Silva Simão, Alexandre Petrenko: Generating checking sequences for partial reduced finite state machines. TestCom/FATES 2008: 153-168

3. Robert M. Hierons, Hasan Ural: Optimizing the length of checking sequences. IEEE Trans. Computers 55(5): 618-629 (2006)

4. Adenilso da Silva Simão, Alexandre Petrenko: Checking completeness of tests for finite state machines. IEEE Trans. Computers 59(8): 1023-1032 (2010)