Testing Real-Time Systems Using Determinization Techniques for Automata over Timed Domains

Abstract

In this work, we are interested in Model-Based Testing for Real-Time Systems. The proposed approach is based on the use of the model of Automata over Timed Domains (ATD) which corresponds to an extension of the classical Timed Automaton Model. First, we explain the main advantages of adopting this new formalism. Then, we propose a testing framework based on ATD and which is an extension of our initial framework presented in previous contributions. We extend the notion of correctness requirements (soundness and completeness) along with the notion of timed input-output conformance relation (tioco) used to compare between implementations and specifications. Moreover we propose a determinization technique used to generate test cases. Finally, several possible extensions of the present work are proposed.

1 Introduction

In general MBT (model based testing) [12] consists in describing the behavior of the SUT (system under test) using a particular adequate formalism and then generating automatically test scenarios from the considered description with respect to some coverage criteria adopting some selection methods. The following step consists in executing the obtained case studies on the SUT and collecting the corresponding verdicts in order to check whether the implementation conforms to its specification or not.

This paper extends some of our previous contributions [5,6,7,8,9] about MBT for real-time systems. Theses works were mainly built on the classical timed automaton model [1]. Our new proposed approach is mainly inspired by [3, 4]. We adopt a new variant of timed automata called automata over timed domains (ATD). This new variant allows to model a much wider class of timed systems and it is equipped with a determinization technique which can be used for test generation. Next in Sect. 2 we propose some definitions related to the proposed formalism. In Sect. 3 we give details about the determinization procedure for ATD. Section 4 introduces the adopted testing framework. Finally Sect. 5 proposes some directions for future work.

2 Definitions

2.1 Timed Domains and Updates

Let $\mathbb {N}$ (respectively $\mathbb {R}{\ge 0}$) be the set of natural numbers (respectively the set of non-negative real-numbers). Timed domains are introduced to represent the progression of continuous entities. A timed domain $\mathcal {D}om$ is made of a set of values denoted by $\mathcal {V}al$ and a time transition function denoted by $\rightsquigarrow$ encoding the progression of those values when time evolves.

Definition 1

A timed domain is a tuple $\mathcal {D}om=\langle \mathcal {V}al,\rightsquigarrow \rangle$ such that:

• $\mathcal {V}al$ is the set of values;

• $\rightsquigarrow : \mathcal {V}al \times \mathbb {R}_{\ge 0} \rightarrow \mathcal {V}al$ is the time transition function such that for all $val\in \mathcal {V}al$ and all $t,t'\in \mathbb {R}_{\ge 0}$ we have $\rightsquigarrow (\rightsquigarrow (val,t),t')=\rightsquigarrow (val,t+t')$.

For simplicity we will write $val \overset{t}{\rightsquigarrow }val'$ instead of $\rightsquigarrow (val,t)=val'$. Moreover we consider the particular symbol $\bot$ which is assigned to the considered resource as soon as it becomes inactive and no longer evolves over time (that is for each $t\in \mathbb {R}_{\ge 0}$ we have $\bot \overset{t}{\rightsquigarrow }\bot$).

For the timed domains $\mathcal {D}om=\langle \mathcal {V}al,\rightsquigarrow _{\mathcal {V}al}\rangle$ and $\mathcal {D}om'=\langle \mathcal {V}al',\rightsquigarrow _{\mathcal {V}al'}\rangle$ we associate the product

$$\mathcal {D}om\times \mathcal {D}om'=\langle \mathcal {V}al_\mathsf {Prod},\rightsquigarrow _\mathsf {Prod}\rangle $$

such that

$$\mathcal {V}al_\mathsf {Prod}=(\mathcal {V}al\cup \{\bot \})\times (\mathcal {V}al'\cup \{\bot \})$$

and for $(val,val')\in \mathcal {V}al_\mathsf {Prod}$ and $t\in \mathbb {R}_{\ge 0}$ we have

$$\rightsquigarrow _{\mathsf {Prod}}\big ((val,val'),t\big )=\big (\rightsquigarrow _{\mathcal {V}al}(val,t),\rightsquigarrow _{\mathcal {V}al'}(val',t)\big ).$$

For $n\in \mathbb {N}_{>1}$, we define the timed domain $\mathcal {D}om^n$ inductively as

$$\mathcal {D}om^1=\mathcal {D}om$$

and

$$\mathcal {D}om^{n+1}=\mathcal {D}om\times \mathcal {D}om^n.$$

Moreover, for $\mathcal {D}om=\langle \mathcal {V}al,\rightsquigarrow _{\mathcal {V}al}\rangle$ we define the timed domain

$$\mathcal {P}(\mathcal {D}om)=\langle \mathcal {V}al_\mathcal {P},\rightsquigarrow _\mathcal {P}\rangle $$

such that

$$\mathcal {V}al_\mathcal {P}=\mathcal {P}(\mathcal {V}al)$$

and

$$\forall V\in \mathcal {V}al_\mathcal {P}\cdot \forall t\in \mathbb {R}_{\ge 0}:\ \rightsquigarrow _\mathcal {P}(V,t)=\{\rightsquigarrow _{\mathcal {V}al}(val,t)\ |\ val\in V\}.$$

Definition 2

Consider a timed domain $\mathcal {D}om=\langle \mathcal {V}al,\rightsquigarrow \rangle$ and an alphabet $\Delta$. An update set for $\mathcal {D}om$ and $\Delta$ is a set $\mathcal {U}\subseteq \Delta \times \mathcal {V}al^{\mathcal {V}al}$.

For an update set $\mathcal {U}$ and a symbol $\delta \in \Delta$, we define the set

$$\mathcal {U}_\delta = \{y\in \mathcal {V}al^{\mathcal {V}al}\ |\ (\delta ,y)\in \mathcal {U}\}.$$

An element from $\mathcal {U}_\delta$ is called a $\delta$-update.¹

Let $\mathcal {D}om$ and $\mathcal {D}om'$ be two timed domains. Moreover consider two update sets $\mathcal {U}$ (for $\mathcal {D}om$ and $\Delta$) and $\mathcal {U'}$ (for $\mathcal {D}om'$ and $\Delta$). We then define the update set $\mathcal {U}\times \mathcal {U'}$ with respect to $\mathcal {D}om\times \mathcal {D}om'$ and $\Delta$ such that

$$\mathcal {U}\times \mathcal {U'}=\big \{\big (\delta ,(y,y')\big )\ | \ \delta \in \Delta \ \wedge \ (y,y')\in \mathcal {U}_\delta \times \mathcal {U'}_\delta \big \}.$$

For $n\in \mathbb {N}_{>1}$, we define the update set $\mathcal {U}^n$ for $\mathcal {D}om^n$ and $\Delta$ inductively as

$$\mathcal {U}^1=\mathcal {U}$$

and

$$\mathcal {U}^{n+1}=\mathcal {U}\times \mathcal {U}^n.$$

We also define the update set $\mathcal {P}(\mathcal {U})$ with respect to $\mathcal {P}(\mathcal {D}om)$ and $\Delta$ such that

$$\mathcal {P}(\mathcal {U})=\big \{\big (\delta ,\mathcal {Y}\big )\in \Delta \times \mathcal {P}(\mathcal {V}al)^{\mathcal {P}(\mathcal {V}al)}\ | \ \forall V\subseteq \mathcal {V}al\cdot \mathcal {Y}(V)=\bigcup _{(y,val)\in \mathcal {U}_\delta \times V}\{y(val)\}\big \}.$$

2.2 Automata over Timed Domains (ATD)

Definition 3

Consider a timed domain $\mathcal {D}om=\langle \mathcal {V}al,\rightsquigarrow \rangle$ and an update set $\mathcal {U}$ for $\mathcal {D}om$ over $\Delta$. An automaton on $\mathcal {D}om$ and $\mathcal {U}$ is a tuple $\mathcal {A} =\langle S, s_{ini}, v_{ini}, E, T\rangle$ where:

• S is a finite set of states;

• $s_{ini}\in S$ is the initial state;

• $val_{ini}\in \mathcal {V}al$ is the initial value;

• $E\subseteq S\times \mathcal {V}al \times \mathcal {U} \times S$ is the set of edges;

• $T\subseteq S$ is the set of terminal states.

For the automaton over timed domains (ATD) $\mathcal {A}$ over $\mathcal {D}om$ and $\mathcal {U}$, we consider the set $C_\mathcal {A}= S\times \mathcal {V}al$ called the set of configurations of $\mathcal {A}$. The ATD $\mathcal {A}$ yiels a timed labeled transition system (TLTS)

$$\mathcal {L_\mathcal {A}}=\langle C_\mathcal {A},c_\mathcal {A}^{ini},\rightarrow _\mathcal {A} \rangle $$

where $c_\mathcal {A}^{ini}$ is the initial configuration of $\mathcal {\mathcal {A}}$ such that

$$c_\mathcal {A}^{ini}=(s_{ini},val_{ini})$$

and

$$\rightarrow _\mathcal {A}=(\overset{t}{\rightarrow }_\mathcal {A})_{t\in \mathbb {R}_{\ge 0}}\uplus (\overset{\delta ,y}{\longrightarrow }_\mathcal {A})_{(\delta ,y)\in \mathcal {U}}$$

such that

• $(s,val)\overset{t}{\rightarrow }_\mathcal {A}(s',val')$ if and only if $s=s'$ and $val \overset{t}{\rightsquigarrow }val'$ ;

• $(s,val)\overset{\delta ,y}{\longrightarrow }_\mathcal {A}{}(s',val')$ if and only if $(s,val,(\delta ,y) , s')\in E$ and $val'=y(val)$.

Similarly, the ATD $\mathcal {A}$ yiels an observable timed labeled transition system (OTLTS)

where

such that

• if and only if $(s,val)\overset{t}{\rightarrow }_\mathcal {A}(s',val')$ ;

• if and only if $\exists y\in \mathcal {V}al^{\mathcal {V}al}:\ (s,val)\overset{\delta ,y}{\longrightarrow }_\mathcal {A}{}(s',val')$.

The first type of transitions is called timed transitions and the second type discrete transitions. For $(s,val)\in C_\mathcal {A}$ and $\mu \in \mathbb {R}_{\ge 0}\uplus \Delta$, we write if there exists $(s',val')\in C_\mathcal {A}$ such that .

2.3 Finitely Representable ATD

A set of guards is a set $\mathcal {G}\subseteq \mathcal {P}(\mathcal {V}al)$. For $\delta \in \Delta$, a $\mathcal {G}$-guarded update for $\delta$ is a couple $(G,\Gamma )\in \mathcal {G}\times \mathcal {P}(\mathcal {U}_\delta )$. For $I\subseteq \mathbb {N}$, consider $\varPsi _I=\{(G_i,\Gamma _i)\ | \ i\in I\}$ a set of $\mathcal {G}$-guarded updates for $\delta$. Also consider $\mathcal {A} =\langle S, s_{ini}, val_{ini}, E, T\rangle$ an automaton on $\mathcal {D}om$ and $\mathcal {U}$. A pair of states $(s,s')$ of $\mathcal {A}$ is said to be compatible with $\varPsi _I$ if the two following conditions hold:

• $\forall \ i\in I. \forall \ val\in G_i. \forall \ y\in \Gamma _i: (s,val,(\delta ,y) , s')\in E$ ;

• $\forall \ (s,val,(\delta ,y) , s')\in E. \exists \ i\in I: v\in G_i \wedge y\in \Gamma _i$ .

Definition 4

The ATD $\mathcal {A}$ is said to be finitely representable using $\mathcal {G}$ if for every pair of states $(s,s')$ of $\mathcal {A}$ and for every $\delta \in \Delta$, there is a finite set $\varPsi$ of $\mathcal {G}$-guarded updates for $\delta$, such that $(s,s')$ is compatible with $\varPsi$.

2.4 Deterministic ATD (DATD)

Consider the ATD $\mathcal {A} =\langle S, s_{ini}, val_{ini}, E, T\rangle$ on $\mathcal {D}om$ and $\mathcal {U}$. Let (s, v) be a possible configuration of $\mathcal {A}$. A timed trace from (s, val) is a sequence $ttr=(s_i,val_i)_{0\le i\le n}$ such that:

• $(s_0,val_0)=(s,val)$ ;

• .

The timed trace ttr is said to be produced by the timed word $tw=(w_i)_{1\le i\le n}$. In this case we write and . The duration of tw is defined as follows

$$\mathcal {D}uration(tw)=\sum _{1\le i \le n} |w_i|$$

where

$$ |w_i|={\left\{ \begin{array}{ll} w_i &{} \text {if} w_i\in \mathbb {R}_{\ge 0}\\ 0 &{} \text {otherwise} \end{array}\right. } $$

that is $\mathcal {D}uration(tw)$ denotes the complete amount of time consumed during the execution of the timed word tw.

In general given a timed word $tw\in (\mathbb {R}_{\ge 0}\uplus \Delta )^*$, the set $TTr_\mathcal {A}((s,val),tw)$ stands for the set of timed traces produced by tw starting from (s, val).

Definition 5

The ATD $\mathcal {A}$ is said to be deterministic if for any timed word $tw\in (\mathbb {R}_{\ge 0}\uplus \Delta )^*$ the cardinality of $TTr_\mathcal {A}((s_{ini},val_{ini}),tw)$ is less or equal to one.

For a positive integer n, we say that the timed word $tw\in (\mathbb {R}_{\ge 0}\uplus \Delta )^n$ is accepted by the ATD $\mathcal {A}$ if there is a timed trace $ttr=(s_i,val_i)_{0\le i\le n}$ such that $ttr\in TTr_\mathcal {A}((s_{ini},val_{ini}),tw)$ and $s_{n+1}\in T$ (i.e. $s_{n+1}$ is a terminal state of $\mathcal {A}$). In this case all the configurations $(s_{i},val_{i})$ are said to be reachable. The set of accepted timed words by $\mathcal {A}$ is denoted $\mathcal {L}ang(\mathcal {A})$ and the set of reachable configurations is denoted $\mathcal {R}each(\mathcal {A})$.

3 Determinization of Non-Deterministic ATD (NDATD)

Consider the (possibly) non-deterministic ATD $\mathcal {A} =\langle S, s_{ini}, val_{ini}, E, T\rangle$ on $\mathcal {D}$ and $\mathcal {U}$ and let $\Delta$ be the alphabet corresponding to the update set $\mathcal {U}$. For simplicity we assume that

$$S=\{s_1,\cdots ,s_p\}$$

such that $p\in \mathbb {N}_{>0}$ and $s_{ini}=s_1$. For every state $s\in S$, we let $\mathsf {index}(s)$ denote the index of s. That is if $s=s_i$ then $\mathsf {index}(s)=i$. For each $1\le i \le p$, we consider the set $Val_i\subseteq \mathcal {V}al$ which corresponds to the set of values corresponding to the state $s_i$.

For $\mathbf {V}=(V_i)_{1\le i\le p}\in \mathcal {P}(\mathcal {V}al)^p$ we consider the set

$$S_\mathbf {V}=\{s\in S\ |\ V_{\mathsf {index}(s)}\ne \emptyset \}$$

which is the group of states the system may occupy when the values for the different states are given by $\mathbf {V}$.

For $\delta \in \Delta$ and $1\le i\le j \le p$, we associate the set

$$\lambda _\delta ^{i\rightarrow j}=\{(val,y)\in \mathcal {V}al\times \mathcal {U}_\delta \ | \ (s_i,val,(\delta ,y) , s_j)\in E\}$$

which corresponds the different ways allowing to move from state $s_i$ to state $s_j$. We also define

$$\lambda _\delta ^{\rightarrow j}=(\lambda _\delta ^{i\rightarrow j})_{1\le i \le p}$$

which in turn records all the ways which allow to reach state $s_j$ starting from any other state of the ATD $\mathcal {A}$.

For the considered letter $\delta$ and each $\lambda _\delta ^{i\rightarrow j}$, we associate the successor function

$$\mathsf {succ}_{\delta ,\lambda _\delta ^{i\rightarrow j}}: \mathcal {V}al\rightarrow \mathcal {P}(\mathcal {V}al)$$

such that for $v\in \mathcal {V}al$ we have

$$\mathsf {succ}_{\delta ,\lambda _\delta ^{i\rightarrow j}}(val)=\{y(val)\ | \ (val,y)\in \lambda _\delta ^{i\rightarrow j}\}$$

which collects all possible obtained values of val after executing instructions in $\lambda _\delta ^{i\rightarrow j}$.

In a natural way we extend $\mathsf {succ}_{\delta ,\lambda _\delta ^{i\rightarrow j}}$ to elements from $\mathcal {P}(\mathcal {V})al$ and we define the function

$$\mathsf {Succ}_{\delta ,\lambda _\delta ^{i\rightarrow j}}: \mathcal {P}(\mathcal {V}al)\rightarrow \mathcal {P}(\mathcal {V}al)$$

such that for $V\subseteq \mathcal {V}al$ we have

$$\mathsf {Succ}_{\delta ,\lambda _\delta ^{i\rightarrow j}}(V)=\bigcup _{val\in V} \mathsf {succ}_{\delta ,\lambda _\delta ^{i\rightarrow j}}(val)$$

which this time collects the possible obtained values of all elements in V after executing instructions in $\lambda _\delta ^{i\rightarrow j}$.

Moreover we define the function

$$\mathsf {Succ}_{\delta ,\lambda _\delta ^{\rightarrow j}}: \mathcal {P}(\mathcal {V}al)^p\rightarrow \mathcal {P}(\mathcal {V}al)$$

such that for $\mathbf {V}=(V_i)_{1\le i\le p}\in \mathcal {P}(\mathcal {V}al)^p$ we have

$$\mathsf {Succ}_{\delta ,\lambda _\delta ^{\rightarrow j}}(\mathbf {V})=\bigcup _{1\le i\le p} \mathsf {Succ}_{\delta ,\lambda _\delta ^{i\rightarrow j}}(V_i)$$

which aggregates the possible updated values of $V_1, \cdots , V_p$ following respectively the instructions in $\delta ^{1\rightarrow j}, \cdots , \delta ^{p\rightarrow j}$.

Furthermore, we define the function

$$\mathsf {Succ}_{\delta ,\mathcal {A}}: \mathcal {P}(\mathcal {V}al)^p\rightarrow \mathcal {P}(\mathcal {V}al)^p$$

such that for $\mathbf {V}al\in \mathcal {P}(\mathcal {V}al)^p$ we have

$$\mathsf {Succ}_{\delta ,\mathcal {A}}(\mathbf {V})=\big (\mathsf {Succ}_{\delta ,\lambda _\delta ^{\rightarrow 1}}(\mathbf {V}),\cdots ,\mathsf {Succ}_{\delta ,\lambda _\delta ^{\rightarrow p}}(\mathbf {V})\big )$$

which can be seen as the successor of $\mathbf {V}$ after the execution of $\delta$.

Lemma 1

Let $\mathbf {V}=(V_i)_{1\le i\le p}\in \mathcal {P}(\mathcal {V}al)^p$ and $\mathbf {V}'=(V'_i)_{1\le i\le p}=\mathsf {Succ}_{\delta ,\mathcal {A}}(\mathbf {V})$. Then for every $s'\in S$ and $v'\in \mathcal {V}$:

$$val'\in {V}'_{\mathsf {index}(s')} \Leftrightarrow \exists (s,val,(\delta ,y) , s')\in E\ s.t.\ v\in {V}_{\mathsf {index}(s)}\ and \ v'=y(val).$$

Finally we define the update set $\mathcal {P}^p(\mathcal {U})$ with respect to $\mathcal {P(D)}^p$ and $\Delta$ such that²

$$\mathcal {P}^p(\mathcal {U})=\{ (\delta ,\mathsf {Succ}_{\delta ,\mathcal {A}})\ | \ \delta \in \Delta \}. $$

We now have all the ingredients to define a deterministic ATD (DATD)

$$\mathcal {A}_{det} =\langle S_{det}, s_{ini}^{det}, val_{ini}^{det}, E_{det}, T_{det}\rangle $$

on $\mathcal {P(D)}^p$ and $\mathcal {P}^p(\mathcal {U})$ which is equivalent to the considered NDATD $\mathcal {A}$. The proposed DATD $\mathcal {A}_{det}$ is defined as follows:

• $S_{det}=\mathcal {P}(S)$;

• $s_{ini}^{det}=\{s_{ini}\}$;

• $val_{ini}^{det}=\big (\{val_{ini}\},\emptyset ,\cdots ,\emptyset \big )\in \mathcal {P}(\mathcal {V})^p$;

• $E_{det}$ is to the set of transitions $(S_{\mathbf {V}},\mathbf {V},(\delta ,\mathsf {Succ}_{\delta ,\mathcal {A}}),S')$ such that $\mathbf {V}\in \mathcal {P}(\mathcal {V}al)^p$ and $S'=S_{\mathbf {V}'}$ with $\mathbf {V}'=\mathsf {Succ}_{\delta ,\mathcal {A}}(\mathbf {V})$;

• $T_{det}=\{S'\subseteq S\ | \ S'\cap T \ne \emptyset \}$.

4 Testing Framework

4.1 ATD with Inputs and Outputs (ATDIO)

Consider the ATD $\mathcal {A} =\langle S, s_{ini}, v_{ini}, E, T\rangle$ on $\mathcal {D}$ and $\mathcal {U}$ and let $\Delta$ be the alphabet corresponding to the update set $\mathcal {U}$. We assume that the alphabet $\Delta$ is split into two disjoint sets namely $\Delta _I$ a set of inputs and $\Delta _O$ a set of outputs (i.e., $\Delta =\Delta _I\sqcup \Delta _O$)³. In this case the ATD $\mathcal {A}$ is called an ATD with inputs and outputs (ATDIO). Moreover for we suppose that all the states of $\mathcal {A}$ are terminal (i.e., $T=E$).

The ATDIO $\mathcal {A}$ is said to be input-enabled if for any reachable configuration $conf\in \mathcal {R}each(\mathcal {A})$ and any input symbol $inp\in \Delta _{I}$ we have .

Moreover the considered ATDIO is called non-blocking if for any reachable configuration $conf\in \mathcal {R}each(\mathcal {A})$ and any duration $t\in \mathbb {R}_{\ge 0}$ there exists $tw\in (\mathbb {R}_{\ge 0} \uplus \Delta _O)^*$ such that and $\mathcal {D}uration(tw)=t$.

Next we suppose that the specification of the system under test and the implementation are given as two non-blocking ATDIO $\mathcal {S}p$ and $\mathcal {I}m$ respectively.⁴

4.2 Parallel Composition of OTLTS with Inputs and Outputs

Given two OTLTS with inputs and outputs $LTS_1$ and $LTS_2$, we define the parallel product $LTS_1||LTS_2$. For $i=1,2$, $LTS_i=(Q_i,q_0^i,\varDelta _\mathsf {I}^i\cup \Delta _{(3-i)\rightarrow i},\varDelta _\mathsf {O}^i\cup \Delta _{i\rightarrow (3- i)},T_d^i,T_t^i)$. The sets $\varDelta _\mathsf {I}^1$, $\varDelta _\mathsf {O}^1$, $\varDelta _\mathsf {I}^2$, $\varDelta _\mathsf {O}^2$, $\Delta _{1\rightarrow 2}$ and $\Delta _{2\rightarrow 1}$ are pairwise disjoint. The two OTLTS synchronize on shared common actions $\Delta _{1\leftrightarrow 2} =\Delta _{1\rightarrow 2}\cup \Delta _{2\rightarrow 1}$ and time delays. The parallel product of the two OTLTS is

$$LTS_1||LTS_2=(Q,(q_0^1,q_0^2),\varDelta _\mathsf {I},\varDelta _\mathsf {O},T_d,T_t)$$

such that

$$\varDelta _\mathsf {I}= \bigcup _{i=1,2}\varDelta _\mathsf {I}^i,\, \varDelta _\mathsf {O}=\bigcup _{i=1,2}\varDelta _\mathsf {O}^i$$

and Q, $T_d$ and $T_t$ are the smallest groups of elements such that:

• $(q_0^1,q_0^2)\in Q$;

• For $(q_1,q_2)\in Q$ and $\delta \in \mathsf {R}$:

  $$ q_1{\mathop {\rightarrow }\limits ^{a}}q'_1\in T_d^1\Rightarrow (q'_1,q_2)\in S\wedge (q_1,q_2){\mathop {\rightarrow }\limits ^{a}}(q'_1,q_2)\in T_d; $$

• For $(q_1,q_2)\in Q$ and $a\in \varDelta _\mathsf {I}^1\cup \varDelta _\mathsf {O}^1\cup \{\tau _1\}$:

  $$q_1{\mathop {\rightarrow }\limits ^{a}}q'_1\in T_d^1\Rightarrow (q'_1,q_2)\in S\wedge (q_1,q_2){\mathop {\rightarrow }\limits ^{a}}(q'_1,q_2)\in T_d; $$

• For $(q_1,q_2)\in Q$ and $a\in \varDelta _\mathsf {I}^2\cup \varDelta _\mathsf {O}^2\cup \{\tau _2\}$:

  $$ q_2{\mathop {\rightarrow }\limits ^{a}}q'_2\in T_d^2\Rightarrow (q_1,q'_2)\in S\wedge (q_1,q_2){\mathop {\rightarrow }\limits ^{a}}(q_1,q'_2)\in T_d; $$

• For $(q_1,q_2)\in Q$ and :

  $$ q_1{\mathop {\rightarrow }\limits ^{a}}q'_1\in T_d^1\wedge q_2{\mathop {\rightarrow }\limits ^{a}}q'_2\in T_d^2\Rightarrow (q'_1,q'_2)\in Q\wedge (q_1,q_2){\mathop {\rightarrow }\limits ^{\tau _a}}(q'_1,q'_2)\in T_d. $$

4.3 Conformance Relation

Given a ATDIO $\mathcal {A}$ and a timed word $tw\in (\mathbb {R}_{\ge 0} \uplus \Delta )^*$, $\mathcal {A} \;\mathsf {after}\; tw$ is the set of configurations of $\mathcal {A}$ that can be reached after the execution of tw. Formally:

Given configuration $conf\in C_\mathcal {A}$, $\mathsf {out}(conf)$ is the set of all observations (either outputs or the elapsing of time) that may happen when the system is at configuration conf. The definition is extended in a natural way to a set of configurations Conf. Formally:

The definition of the relation $\mathsf {tioco}$ [10, 11] is as follows:

$$\mathcal {I}m \;\mathsf {tioco}\; \mathcal {S}p\ \ \textit{iff}\ \ \forall tw \in \mathcal {L}ang(\mathcal {S}p) \;:\; \mathsf {out}(\mathcal {I}m \;\mathsf {after}\; tw) \subseteq \mathsf {out}(\mathcal {S}p \;\mathsf {after}\; tw). $$

The relation indicates that the implementation $\mathcal {I}m$ conforms to the specification $\mathcal {S}p$ if and only if for any timed word tw of $\mathcal {S}p$, the set of outputs (including time elapse) of $\mathcal {I}m$ after the execution of tw is a subset of the set of outputs that can be generated by $\mathcal {S}p$.

4.4 Timed Test Cases

A timed test case for the specification $\mathcal {S}p$ over is a total function

$$ TTest : (\mathbb {R}_{\ge 0} \uplus \Delta )^* \rightarrow \varDelta _\mathsf {I}\cup \{\mathsf {WT},\mathsf {PS},\mathsf {FL}\}. $$

TTest(tw) indicates the action that must executed by the tester once it observes tw. If $TTest(tw)=inp\in \varDelta _\mathsf {I}$ then the tester produces input inp. If $TTest(tw)=\mathsf {WT}$ then the tester lets time elapse (waits). If $TTest(tw)\in \{\mathsf {PS},\mathsf {FL}\}$ then the tester emits a verdict and stops.

The execution of TTest on $\mathcal {I}m$ may be seen as the parallel composition of the OTLTS with inputs and outputs defined by TTest and $\mathcal {I}m$. The product TIOLTS is denoted by $\mathcal {I}m \Vert TTest$. In a formal fashion, we announce that the implementation $\mathcal {I}m$ passes TTest, denoted $\mathcal {I}m \;\mathsf {passes}\; TTest$, if state $\mathsf {FL}$ can not be reached in $\mathcal {I}m \Vert TTest$. We declare that the implementation passes (respectively fails) the test suite $\mathcal{{TT}}$ if it passes all tests (respectively fails at least one test) in $\mathcal{{TT}}$. $\mathcal{{TT}}$ is said to be sound with respect to $\mathcal {S}p$ if

$$\forall \mathcal {I}m \;:\; \mathcal {I}m \;\mathsf {tioco}\; \mathcal {S}p \Rightarrow \mathcal {I}m \;\mathsf {passes}\; \mathcal{{TT}}.$$

Similarly $\mathcal{{TT}}$ is said to be complete with respect to $\mathcal {S}p$ if

$$\forall \mathcal {I}m \;:\; \mathcal {I}m \;\mathsf {passes}\; \mathcal{{TT}}\Rightarrow \mathcal {I}m \;\mathsf {tioco}\; \mathcal {S}p.$$

Our goal it then to produce test suites which are both sound and complete. More precisely, we aim to generate timed tests in the form of deterministic ATDIO and which are finitely representable. For that purpose we need to use the determinization technique proposed in Sect. 3.

5 Future Work

The work proposed in this paper is at its beginning. In the future we need to work on many aspects:

• First, we need to extend the presented framework to the case where the specification of the SUT is given as a product of ATDIO and not simply one ATDIO. In this way we can deal with distributed and multi-components systems.

• Second, we should find a way which guarantees that the generated timed tests are finitely representable so that we can store them and execute them later on. For that, we need to use some approximation techniques based on game theory techniques like the ones proposed in [2].

• Third, we need to use some coverage and selection techniques which allow to reduce the size of generated test cases and to efficiently deal the state explosion problem usually encountered when following model-based approaches.