Constraint-Based Oracles for Timed Distributed Systems

Abstract

This paper studies the situation in which the system under test and the system model are distributed and have the same structure; they have corresponding remote components that communicate asynchronously. In testing, a component with interface $C_i$ has its own local tester that interacts with $C_i$ and this local tester observes a local trace consisting of inputs, outputs and durations as perceived by $C_i$. An observation made in testing is thus a multi-trace: a tuple of (timed) local traces, one for each $C_i$. The conformance relation for such distributed systems combines a classical unitary conformance relation for localised components and the requirement that the communication policy was satisfied. By expressing the communication policy as a constraint satisfaction problem, we were able to implement the computation of test verdicts by orchestrating localised off-line testing algorithms and the verification of constraints defined by message passing between components. Lastly, we illustrate our approach on a telecommunications system.

1 Introduction

Distributed systems can be seen as collections of physically remote reactive systems communicating through communication media. The classical approach to testing such systems involves placing a local tester at each localised interface, with each local tester only observing the events at its interface. If testers do not exchange synchronisation messages and there is no global clock, this corresponds to the ISO standardised distributed test architecture [11]. The result of test execution can be modelled as a collection of logs (local traces); each is a sequence of messages involving a given localised system.

Model-Based Testing (MBT) [8, 17, 21] aims to automate three central processes in testing, namely: the test generation process whose purpose is to extract test cases from a behavioural model of the System Under Test (SUT), the test execution process whose purpose is to orchestrate the stimulation of the SUT with input test data and the collection of the SUT’s reactions and finally, the verdict (oracle) computation phase whose purpose is to analyse the results of test case executions, given as execution traces, in order to identify faults by checking traces against the model¹. This comparison is based on a conformance relation that relates traces of SUTs and traces of their associated models.

MBT was first explored in a centralised context but extensions to distributed SUTs have been defined, initially motivated by protocol conformance testing [19]. This includes work that uses Input Output Transition System (IOTS) as the modelling formalism [3, 9, 10]. In the context of distributed testing from Timed IOTS (TIOTS), in [6], we extended the tioco conformance relation [14, 15, 20] to define a conformance relation dtioco for timed distributed testing. The model of a distributed SUT is given as a tuple of TIOTSs, each modelling one of the localised subsystems of the SUT. The result of test case execution is a tuple of timed traces (a timed trace is a trace in which delays between consecutive interactions of the tester with the localised SUT are recorded). Under the hypothesis that localised systems communicate in a multi-cast mode, we have shown that the verdict computation process can be conducted by combining centralised MBT techniques for each localised system, using the tioco conformance relation, and a step-by-step algorithm whose purpose is to check that the tuple of timed traces is consistent with the underlying communication hypothesis [6].

The goal of this paper is twofold. First, we propose an improvement of the algorithm presented in [6] by formulating the oracle problem as a constraint solving problem. While the previous algorithm analyses a multi-trace by mimicking step by step emissions and receptions of messages, as well as the passage of time, in this article, we reformulate the verification of message passing as a set of inequality constraints that can be supported by a constraint solver. Compared to the one introduced in [6], the new algorithm treats durations between communication actions as real numbers. In [6] those durations had to be representable as multiples of a basic time unit, which only allowed us to consider durations in a set isomorphic to the set of natural numbers. The previous approach also included backtracking. In the new algorithm, durations may be any real number that falls in the theory addressed by the considered solver. Second, we present the tool that solves the oracle problem using both a localised verdict computation approach for tioco (presented in [1]) and the verification of constraints to check internal communications between localised systems. We consider a case study modelling a telecommunication system, named PhoneX [18] specified as a collection of Timed Input Output Symbolic Transition Systems (TIOSTS), which are symbolic representations of TIOTS.

Section 2 introduces the types of models used and Sect. 3 presents the PhoneX case study. Section 4 recalls the testing framework and introduces the verification of message passing using constraints. Section 5 describes a scalability study, based on the PhoneX example, that applied mutation techniques to generate correct and faulty trace tuples. Section 6 discusses related works and Sect. 7 gives concluding remarks.

2 Modelling Framework

2.1 TIOSTS

Timed Input Output Symbolic Transition Systems (TIOSTS) are symbolic automata built over a signature $\varSigma =(\varOmega ,A,T, C)$ where $\varOmega =(S,F)$ is an equational logic signature with S a set of types and F a set of functions provided with an arity. The functions are interpreted in a model M as usual. A is a set of data variables used to store input values, to denote system state evolutions and to define guards. T is a set of clocks, which are variables whose values are elements of a set D isomorphic to non-negative real numbers and that are used to denote durations. $D^+$ will denote $D\setminus \{ 0\}$. M is supposed to contain D. Variables in $A\cup T$ are assigned values by interpretations of the form $\nu : A\cup T \rightarrow M$; $M^{A\cup T}$ is the set of all interpretations. Finally, C is a set of channels partitioned as $C^{in}\coprod C^{out}$ where elements of $C^{in}$ (resp. $C^{out}$) are input (resp. output) channels. The set of terms $T_\varOmega (A)$ over $\varOmega$ and A is inductively defined as usual and variable interpretations are canonically extended to terms. The set of symbolic actions $Act(\varSigma )$ is $I(\varSigma )\cup O(\varSigma )$ with $I(\varSigma )= \{c?x~|~x \in A, c\in C^{in} \}$ and $O(\varSigma )=\{ c!t~|~t \in T_\varOmega (A), c\in C^{out}\}$. In order to simplify the exposition, at the level of our modelling framework, we consider messages that contain only a single piece of data. However, at the tooling level, without adding any particular difficulties, messages contain 0 (signals c! or c?), 1 or n data ($c!(t_1,\ldots ,t_n)$ or $c?(x_1,\ldots ,x_n)$, the $x_i$ being different variables of A).

A TIOSTS is a triple $\mathbb {G}=(Q, q_0,Tr)$ where Q is a set of states, $q_0$ is a distinguished element of Q called the initial state, and Tr is a set of labeled transitions. A transition is defined by a tuple $(q,\phi ,\psi ,\mathbb {T},act,\rho ,q')$ where q (resp. $q'$) is the source (resp. target) state of the transition, $\phi$ is a formula, called time guard, of the form $z \le Cst$ or $z \ge Cst$ where $z \in T$ and Cst is a constant interpreted in D ($\phi$ constrains the delay at which the action act occurs), $\psi$ is an equational logic formula, called data guard ($\psi$ is a firing condition on attribute variables), $\mathbb {T} \subseteq T$ is a set of time variables (to be reset to 0 when the transition is executed), act is a communication action and $\rho$ assigns terms of $T_\varOmega (A)$ to variables in A in order to represent state evolutions. In the sequel, we use $M\,\models _\nu \,\varphi$ to say that $\varphi$ holds for interpretation $\nu$. The set of paths of $\mathbb {G}$ contains the empty sequence $\varepsilon$ and all sequences $tr_1 . \cdots .tr_n$ of transitions of Tr such that $source(tr_1)=q_0$ and for all $i<n$, $target(tr_i)=source(tr_{i+1})$.

Concrete actions are values exchanged through channels. The set of concrete actions over C is thus $Act(C)=I(C)\cup O(C)$ where $I(C)=\{c?v~|~c\in C^{in}, v\in M\}$ are inputs and $O(C)=\{c!v~|~c\in C^{out}, v\in M\}$ are outputs. Given $act \in Act(C)$ of the form $c\varDelta v$ with $\varDelta \in \{!,?\}$, chan(act) refers to c, $\overline{act}$ refers to its mirror action, $c \overline{\varDelta } v$ with $\overline{!}=?$ and $\overline{?}=!$. Variable interpretations are canonically extended to symbolic actions ($\nu (c?x)= c?(\nu (x))$ and $\nu (c!t)=c!\nu (t)$).

A concrete action is generally observed after a delay has occurred since the previous occurrence of a concrete action. This is captured by the notion of events.

Definition 1

(Events). The set of (resp. initialised) events over C is defined as $Evt(C)=(D^+\cup \{\_\}) \times (Act(C) \cup \{\delta \})$ (resp. $IEvt(C)= D^+ \times (Act(C) \cup \{\delta \})$).

Pair (d, a) represents the observation of concrete action a after delay d. Following [21], symbol ‘$\delta$’ is used to denote the absence of observation of a concrete action (i.e. quiescence). Let us point out that usually, in a pure timed framework, $\delta$ may be useless (e.g. [6, 13, 14]). Here, the use of $\delta$ is a side effect of considering atomic actions as events. Indeed, expressing that a system is quiescent after a duration d has to be representable as an event, and thus, we need a symbol to represent these quiescent situations as a couple $(d,\delta )$. Symbol ‘$\_$’ is introduced to denote the absence of the observation of a delay (i.e. $(\_,a)$). We require this so that the first action of a localised trace need not be stamped with a duration. In addition, between two consecutive concrete actions on one location, we require that the delay is greater than zero so that two events do not occur simultaneously. Given $ev \in Evt(C)$, we let $act(ev)=a$ and $delay(ev)=d$ if $ev=(d,a)$ with $d \in D^+$, else $delay(ev)=0$ ($ev =(\_,a)$). In the sequel $\delta Evt(C)$ denotes $\{ ev\in Evt(C) \backslash act(ev)=\delta \}$.

Definition 2

(Timed traces). The set ITraces(C) of initialised traces over C is² .

The set UTraces(C) of uninitialised traces over C is $\{ u(\sigma )~|~\sigma \in ITraces(C)\}$ where $u(\sigma )$ denotes $\varepsilon$ if .

The set TTraces(C) of timed traces over C is $UTraces(C)\cup ITraces(C)$.

Any event of an initialised trace contains a duration and a concrete action. For the first event, this duration represents a delay between some distinguished moment (e.g. since the time at which a tester started to measure the duration) and the first observed action. Uninitialised traces are timed traces for which no initial instant is identified. Finally, note that quiescence is only observed at the end of traces, when no communication action follows it. Indeed when a communication action a occurs after a period of time where an implementation remains silent, this period of time is captured by the delay of the event introducing a.

For $\sigma \in TTraces(C)$, $dur(\sigma )$ denotes the duration of $\sigma$, which is 0 if $\sigma$ is $\varepsilon$, and otherwise is the sum of all delays of events in $\sigma$. $Pref(\sigma )$ denotes the set of prefixes of $\sigma$ defined as $\{ \varepsilon \}$ if $\sigma$ is $\varepsilon$ and $Pref(\sigma ')\cup \{\sigma \}$ if $\sigma$ is of the form . Moreover, for an action a in Act(C), $|\sigma |_a$ denotes the number of occurrences of a in $\sigma$. $pref(\sigma , a, n)$ stands for the smallest prefix of $\sigma$ that contains n occurrences of a when this prefix exists. Finally, using the pref operation, we introduce an operation that measures the elapsed time at the nth occurrence of an event a from the beginning of the trace. By convention, if a trace contains strictly fewer than n occurrences of a, then the associated duration is that of the entire trace.

$$ dur\_occ(\sigma , a,n) = \left\{ \begin{array}{ll} dur( pref(\sigma , a, n) ) &{} \text{ if } pref(\sigma , a, n) \text{ exists } \\ dur(\sigma ) &{} \text{ else } \end{array}\right. $$

We now define runs of transitions of TIOSTS:

Definition 3

(Runs of transitions). Let $\mathbb {G}=(Q,q_0,Tr)$ be a TIOSTS over $\varSigma$. The set $Snp_M(\mathbb {G})$ of snapshots of $\mathbb {G}$ is the set $Q \times M^{A\cup T}$. For $tr=(q,{\phi },{\psi },\mathbb {T},act,\rho ,q') \in Tr$, the set of runs of tr is the set $Run(tr)\subseteq Snp_M(\mathbb {G})\times Evt(C)\times Snp_M(\mathbb {G})$ s.t. $((q,\nu ) ,ev ,$ $(q',\nu '))\in Run(tr)$ iff there exist $d\in D$ and $\xi :A\cup T\rightarrow M$ satisfying:

• for all $w\in T$, $\xi (w)= \nu (w)+ d$,

• if $act=c!t$ then for all $x\in A$, $\xi (x)=\nu (x)$, else ($act= c?x$) for all $y\in A\setminus \{ x\}$, $\xi (y)=\nu (y)$,

and such that we have either $ev =(d,\xi (act))$ or $ev =(\_,\xi (act))$, $\forall x \in A, \nu '(x)=\xi (\rho (x))$, $\forall w\in \mathbb {T}$, $\nu '(w)=0$, $\forall w\in (T \setminus \mathbb {T}), \nu '(w)=\xi (w)$, $M\,\models _{\xi }\,\phi$ and $M\,\models _{\xi }\,\psi$.

In Definition 3, $\xi$ is an intermediate interpretation whose purpose is to let time pass from $\nu$ for all clocks ($\xi (w)= \nu (w)+ d$) and take into account a potential input value (denoted by $\xi (x)$ if $act= c?x$). Guards of the transition should be satisfied by $\xi$ and if it is the case then the transition can be fired resulting on a new interpretation $\nu '$ updating data variables according to $\rho$ and resetting clocks occurring in $\mathbb {T}$.

For a path p of $\mathbb {G}$, the set of timed traces of p, denoted TTraces(p) is $\{\varepsilon \}$ if $p=\varepsilon$ and if p is of the form $tr_1. \cdots .tr_n$, TTrace(p) contains all sequences of events $ev_1 \cdots ev_n$ such that there exists a sequence of runs $r_1 \cdots r_n$ satisfying: for all $i\le n$, $r_i$ is a run of $tr_i$ of the form $(snp_i ,ev_i , snp'_{i+1})$ and for all $j<n$ we have $snp'_j =snp_{j+1}$ and such that all events are initialised except for $i= 1$, i.e. $ev_1$ is of form $(\_,a_1)$ and for all $i >1$, $ev_i$ is of form $(d_i,a_i)$.

By taking into account the particular action $\delta$, the set of timed traces of $\mathbb {G}$, denoted $TTraces(\mathbb {G})$, is defined as:

• For all $p\in Path(\mathbb {G})$ we have $TTraces(p)\subseteq TTraces(\mathbb {G})$,

• For all $\sigma \in TTraces(\mathbb {G})$ such that there exists no path p and no event ev with $act(ev)\in O(C)$ satisfying $\sigma . ev \in TTraces(p)$, we have $\sigma .(d,\delta ) \in TTraces(\mathbb {G})$ if $\sigma \ne \varepsilon$ and $(\_,\delta ) \in TTraces(\mathbb {G})$ if $\sigma =\varepsilon$.

2.2 Communication and Systems

We now define a distributed interface as a collection of localised interfaces.

Definition 4

(Distributed interface). A distributed interface is a tuple $\varLambda =(C_1,\cdots ,C_n)$, with $n\ge 1$, where for all $i\le n$, $C_i$ is a set of channels such that for any $i\ne j$ we have $C^{out}_i \cap C^{out}_j =\emptyset$. $C(\varLambda )$, which is equal to $\bigcup _{i\le n} C_i$, is the set of channels of $\varLambda$ with $C(\varLambda )^{in}=\bigcup _{i\le n}C^{in}_i$ and $C(\varLambda )^{out}=\bigcup _{i\le n}C^{out}_i$.

$C^{out}_i \cap C^{out}_j =\emptyset$ ensures that for a channel c, messages emitted through c can only be emitted from one sender. This is a simplification hypothesis that makes the later formalisation lighter. In a distributed architecture, for a given localised interface $C_i$ of $\varLambda =(C_1,\cdots ,C_n)$, $C_i^{int}$ (resp. $C_i^{ext}$), defined as $\bigcup \{C_i\cap C_j~|~j\le n \wedge j\ne i\}$ (resp. $C_i\backslash C_i^{int}$), denotes the set of internal channels (resp. external channels) that can be used to exchange messages with other localised subsystems (resp. exchange messages with the system environment). We let $C^{int}(\varLambda )$ denote $\bigcup _{i\le n} C^{int}_i$, $C^{ext}(\varLambda )$ denote $\bigcup _{i\le n} C^{ext}_i$, and $Act(\varLambda )$ denote $I(\varLambda )\cup O(\varLambda )$ with $I(\varLambda )=\bigcup _{i\le n}I(C_i)$ and $O(\varLambda )=\bigcup _{i\le n}O(C_i)$. $I^{int}(\varLambda )$ (resp. $O^{int}(\varLambda )$) is the subset of $I(\varLambda )$ (resp. $O(\varLambda )$) whose elements are inputs (resp. outputs) through internal channels. For any $c!v\in O(\varLambda )$, $Sender(\varLambda , c!v)$ stands for the index j such that $c\in C^{out}_j$. We let $Act^{int}(\varLambda )=I^{int}(\varLambda )\cup O^{int}(\varLambda )$, $Evt(\varLambda ) = Evt(C(\varLambda ))$, and $Evt^{int}_{in}(\varLambda )$ be the set of events whose action is an internal input. We define $Tup(\varLambda )$ to be $TTraces(C_1)\times \cdots \times TTraces(C_n)$. In the sequel, a distributed interface $\varLambda =(C_1,\cdots ,C_n)$ is given. An observation made in a system will be a tuple of timed traces where each timed trace represents a local observation. We first introduce the notion of a multi-trace, which is a tuple of timed traces characterising compatible communications between a collection of localised subsystems.

Definition 5

(Multi-traces). The set of multi-traces of $\varLambda$ with initial instants, denoted $IMTraces(\varLambda )$, is the subset of $ITraces(C_1)\times \cdots \times ITraces(C_n)$ defined as follows:

• Empty multi-trace: $(\varepsilon ,\cdots ,\varepsilon )\in IMTraces(\varLambda )$,

• multi-trace Extension: for any $\mu =(\sigma _1,\dots ,\sigma _n)\in IMTraces(\varLambda )$, for $ev\in IEvt(C_i)$ for $i\le n$, $(\sigma _1,\dots ,\sigma _i .ev,\dots ,\sigma _n) \in IMTraces(\varLambda )$ provided that: if $act(ev) \in I(C_i)\cap I^{int}(\varLambda )$, we have $|\sigma _j|_{\overline{ev}} \ge |\sigma _i|_{act(ev)} +1$ and with $j = Sender(\varLambda ,\overline{act(ev)})$.

The set $UMTraces(\varLambda )$ (resp. $MTraces(\varLambda )$) of uninitialised multi-traces (resp. of multi-traces) of $\varLambda$ is $\{ (u(\sigma _1),\cdots ,u(\sigma _n))~|~(\sigma _1,\cdots ,\sigma _n)\in IMTraces(\varLambda ) \}$ (resp. $UMTraces(\varLambda ) \cup IMTraces(\varLambda )$).

Initialised multi-traces denote tuples of traces, each trace of the tuple being a partial centralised vision of a common distributed execution. The nature of communication considered is multicast, as captured by the property that an internal message can be received at some $C_i$ only if $C_i$ has consumed fewer occurrences of this message than the number of the corresponding output occurrences. Each trace occurring in an initialised multi-trace starts with an event introducing a duration. All those durations are supposed to start at a common initial instant. Of course, in the context of distributed executions it is generally not possible to observe such a common initial instant. Therefore, we defined uninitialised multi-traces in which the initial durations are not observable. Similar rules have been proposed in [16] to express component composition in a distributed setting.

In distributed testing, we assume that there is a separate tester at each localised interface and there is no global clock for globally ordering distributed events. Hence, we cannot make any assumption on the different moments at which the different local testers stop observing their associated interfaces. To capture this, we accept as valid observations, tuples made of multi-trace prefixes.

Definition 6

(Observable multi-traces). The set of initialised observable multi-traces of $\varLambda$, denoted $IOTraces(\varLambda )$, is the smallest set containing $IMTraces(\varLambda )$ and such that for any $(\sigma _1,\cdots ,\sigma _i .ev,\cdots ,\sigma _n)\in IOTraces(\varLambda )$ we have $(\sigma _1,\cdots ,\sigma _n)\in IOTraces(\varLambda )$.

The set of uninitialised observable multi-traces of $\varLambda$, denoted $UOTraces(\varLambda )$, is the set $\{ (u(\sigma _1),\cdots ,u(\sigma _n))~|~(\sigma _1,\cdots ,\sigma _n)\in IOTraces(\varLambda )\}$.

Initialised observable multi-traces characterise observations starting at a common initial instant but ending at different instants depending on the considered component of the interface. Of course, since there is a common initial instant it is possible to order the moments at which the observations of the different traces of the tuple occur ($\sigma _i$ ends before $\sigma _j$ if $dur(\sigma _i) < dur(\sigma _j)$). However, in general such an initial instant cannot be identified in testing. Therefore, real observations of system executions should be defined by tuples containing only uninitialised traces, which is captured by uninitialised observable multi-traces.

Definition 7

Let $\varLambda =(C_1,\cdots ,C_n)$ be a distributed interface. A system over $\varLambda$ is a tuple $Sys=(\mathbb {G}_1 ,\cdots \mathbb {G}_n)$ such that for all $i\le n$ we have $\mathbb {G}_i$ is a TIOSTS over a signature of the form $(\varOmega _i ,A_i,T_i, C_i)$. The semantics of Sys, denoted TTraces(Sys) is defined as $(TTraces(\mathbb {G}_1) \times \cdots \times TTraces(\mathbb {G}_n)) \cap \,UOTraces(\varLambda )$.

3 The PhoneX Case Study

PhoneX [18] is a central telecommunication system model describing a protocol to establish sessions between phones. It was initially used as a reference to investigate the test case generation capacities of the platform Diversity³ by the Ericsson company. In our context, PhoneX is interesting since it allows the number of communicating actors to be parameterised, even though there is only one time constraint in the subsystem models. Figure 1 depicts a scenario of a successful session setup and call establishment between 2 phones. A caller with $Phone_{112}$ initiates a call (doCall(113)) to the user of $Phone_{113}$. The PhoneX server, after receiving Calling(112, 113), checks if $Phone_{113}$ is registered, available, and then starts StartSession(112, 113) for communication management and remains available. $Session_{112}^{113}$ informs $Phone_{113}$ that $Phone_{112}$ tried to get in contact (CalledBy(112)). The user of $Phone_{113}$ can accept the call (doAcceptCall) and informs $Session_{112}^{113}$ using AcceptingCall which can establish communication (multicasting InitCall). Each user can end the call (the user of $Phone_{112}$ hangs up, doEndCall) and report it (EndingCall) to $Session_{112}^{113}$ that closes the connection by multicasting TermCall and becomes available (EndSession(112, 113)) again. Figure 2 depicts the architecture. Components $Caller Client$ and $Called Client$ define two roles that registered phones can have. PhoneX is the component that plays the role of the telecommunication centre. $Active Session$ is a generic representation of sessions created by the centre to manage communications between phones. Communication channels model the media used by components in Fig. 2.

Fig. 1.

Interaction scenario of a successful call operation

Fig. 2.

The PhoneX architecture

Caller client behaviour (Fig. 3(a)). At the Idle state, caller src receives a call from the environment (a caller) to make a call operation with called dest. Then it joins PhoneX central by sending to it src and dest (caller reaches Initiating state). Caller returns to Idle state when it receives an error code from PhoneX (PhoneX cannot establish a call due to violated condition of call establishment) or a signal to terminate the call from the active session (due to a call rejection by called client). At Initiating, src may reach Established if a call is established by active session or state Terminating if a no-answer (from called client) is observed during a waiting delay. When a call is established (at Established), src may return to Idle by receiving a terminating signal from the active session (due to an ending call by called client) or receive a signal from the environment (a caller) to end the call in progress (caller reaches UserEndingCall). At UserEndingCall, the caller notifies the active session for terminating the call (caller reaches Terminating). At Terminating, src returns to Idle by receiving a terminating signal from the active session.

Called client behaviour (Fig. 3(b)). This role is symmetric (on the called client side) to the one described in Fig. 3(a)).

Fig. 3.

TIOSTSs $\mathbb {G}_{src}$ and $\mathbb {G}_{dest}$ of Caller and Called clients

PhoneX central behaviour (Fig. 4(a)). At the Idle state, PhoneX may receive a call and reach Calling or get notified of the ending of an already active session and return to Idle. At Calling, PhoneX may start a new session (src, dest) and return to Idle provided that dest is a registered and allowed-to-call number in the Client database and there is no active session with called client dest. Otherwise, PhoneX may also return to Idle when dest is not registered in Client database, or calling dest is not allowed, or called client dest is busy.

Session behaviour (depicted in Fig. 4(b)). When a new session is started, a Session TIOSTS is instantiated. At the Idle state, Session receives src and dest numbers, it then reaches Starting. It notifies dest with a call operation emitted by src and reaches Initiating. At Initiating, it may reach either Accepted when called client accepts the call during a waiting delay or Terminating if a no-answer is observed during a waiting delay or the call get rejected. At Accepted, active session initiates a call between src and dest and reaches state Established. Then, either caller or called client may end the call (session reaches Terminating state). At Terminating state session sends a terminating signal to both caller and called clients and reaches Ending. Finally, it returns to Idle by notifying PhoneX central of ending the active session.

Fig. 4.

TIOSTSs $\mathbb {G}_{X}$ and $\mathbb {G}_{S}$ of PhoneX Central and Active Session

4 Testing

In [6], we modelled timed distributed systems as tuples $(\mathbb {LS}_1,\dots ,\mathbb {LS}_n)$ where each $\mathbb {LS}_i$ denotes a black box localised system under test. Then we defined a conformance relation dtioco to test such a distributed system with respect to a system model $(\mathbb {G}_1,\dots ,\mathbb {G}_n)$. We showed that solving the oracle problem for an observable multi-trace $(\sigma _1,\cdots ,\sigma _n)$ reduces to: (a) solve the oracle problem of each $\sigma _i$ with respect to tioco [15] and with $\mathbb {G}_i$ as reference model (unitary testing, see Sect. 4.1) and, (b) check whether $(\sigma _1,\cdots ,\sigma _n)$ is an observable (uninitialised) multi-trace. In Sect. 4.1 we briefly recall the principles of a simplified⁴ version of the unitary testing algorithm defined in [1]. Then in Sect. 4.2, we introduce the new algorithm based on constraint solving to decide if a tuple is an observational multi-trace. As compared to [1, 6], we have slightly adapted our definitions of timed traces in order to deal with events instead of atomic observations such as inputs, outputs or durations; this adaptation has no impact on the results in [1, 6].

4.1 Unitary Testing

A Localised subsystem Under Test (LUT) is defined over a set of channels C as a non-empty subset $\mathbb {LS}$ of UOTraces(C) such that:

• Input completeness: for any $\sigma$ in $\mathbb {LS}$ of the form , for any $ev\in Evt(C)$ such that $act(ev)\in I(C)$ and $delay(ev)\le delay(ev')$, we have .

• Quiescence: for all $\sigma \in \mathbb {LS}$ we have:

  $$\forall ev\in Evt(C). (act(ev)\in O(C) \Rightarrow \sigma .ev \notin \mathbb {LS})$$
  $$\Leftrightarrow $$
  $$(\sigma \ne \varepsilon \Rightarrow (\forall d\in D^+,\sigma .(d,\delta ) \in \mathbb {LS})) \wedge (\sigma =\varepsilon \Rightarrow (\_,\delta ) \in \mathbb {LS})$$

  Moreover for any $\sigma$ in $\mathbb {LS}$ of the form with $act(ev')=\delta$, for any $ev\in Evt(C)$ with $act(ev)\in O(C)$ we have .

• Reaction prefix: for any $\sigma$ in $\mathbb {LS}$, we have $Pref(\sigma )\subseteq \mathbb {LS}$.

Input completeness is required so that an LUT cannot refuse an input from the environment. Quiescence corresponds to situations where the LUT will not react anymore until it receives a new stimulation. Reaction prefix is a realistic property stating that a prefix of an observation is an observation.

The local verdict computation algorithm is based on a symbolic structure $SE(\mathbb {G})_\delta$ computed from the reference model $\mathbb {G}$ obtained by classical symbolic execution techniques. It is a tree-like structure whose nodes are symbolic states used to capture information related to the possible executions of $\mathbb {G}$. A path p is a sequence of consecutive edges relating symbolic states and labelled by symbolic events. The set of executions (uninitialised timed traces) associated to p is characterised by the sequence $ev_1\cdots ev_n$ of symbolic events labelling the consecutive edges and by the final symbolic state $\eta$. Each symbolic event of the sequence is of the form $(d_i, act_i)$ (except $ev_1$ which is of the form $(\_ ,act_1)$). Each $d_i$ is a new fresh variable (i.e. not used in the definition of $\mathbb {G}$) used to represent durations (they are typed as clocks) and each $act_i$ is of the form $c?z_i$ or $c!t_i$ where $z_i$ is a new fresh variable and $t_i$ is a term built over the same equational logic signature $\varOmega$ as terms in $\mathbb {G}$ but on a set of new fresh variables. $\eta$ is of the form $(q, \pi _d ,\pi _t , \varrho )$ where q is the state reached in $\mathbb {G}$, $\pi _d$ is a constraint on new fresh data variables (let $F_d$ be the set of those variables), $\pi _t$ is a constraint on the set of variables of the form $d_i$ and $\varrho :A\rightarrow T_\varOmega (F_d)$ associates symbolic values to variables of $\mathbb {G}$. An uninitialised timed trace $ev'_1 \cdots ev'_n$ belongs to p iff for all $i\le n$:

• $ev'_i$ is of the form $(\_ ,act'_i)$ (resp. $(d'_i , act'_i)$) if $ev_i$ is of the form $(\_ ,act_i)$ (resp. $(d_i, act_i)$) and $act'_i$ is of the form $c?z'_i$ (resp. $c!t'_i$) if $act_i$ is of the form $c?z_i$ (resp. $c!t_i$).

• Let $x_i$ (resp. $x'_i$) stand for the variable $z_i$ (resp. $z'_i$) if $act_i$ (resp. $act'_i$) is an input and for the term $t_i$ (resp. $t'_i$) if $act_i$ (resp. $act'_i$) is an output. The formula $(\bigwedge _{i\le n} x_i = x'_i)\wedge \pi _d \wedge \pi _t$ is satisfiable.

The verdict computation algorithm analyses successively all events of $\sigma = ev'_1 \cdots ev'_n$ and at each steps it computes the set of paths to which the already analysed prefix of $\sigma$ belongs. As soon as possible a verdict is emitted⁵:

• Fail if $act(ev'_i)$ is an output or $\delta$ and the set of path becomes empty, or else $act(ev'_i)$ is an input $(d'_i , act'_i)$ and there exists an event $ev''_i =(d''_i,act''_i)$ where $act''_i$ is an output (not $\delta$) satisfying $d''_i <d'_i$ and $ev'_1 \cdots ev'_{i-1}.ev''_i$ belongs to some path of $SE(\mathbb {G})_\delta$.

• Inconc if $act(ev'_i)$ is an input $(d'_i , act'_i)$, the set of path becomes empty, and for all events $ev''_i =(d''_i,act''_i)$ where $act''_i$ is an output (not $\delta$), $d''_i <d'_i$ we have $ev'_1 \cdots ev'_{i-1}.ev''_i$ does not belong to any path of $SE(\mathbb {G})_\delta$.

• Pass if $\sigma$ is fully analysed without generating any of the previous verdicts.

4.2 Communication Testing

An SUT over $\varLambda$ is a tuple $\mathbb {S} = (\mathbb {LS}_1,\dots ,\mathbb {LS}_n)$ where $\mathbb {LS}_i$ is an LUT defined over $C_i$ (all $i\le n$). The semantics of $\mathbb {S}$, denoted $Obs(\mathbb {S})\subseteq \mathbb {LS}_1\times \dots \times \mathbb {LS}_n$, contains all observations that can be made when executing $\mathbb {S}$. The goal of Algorithm 1 is to check whether those observations reveal communication errors by checking whether they are in $UOTraces(\varLambda )$. It is based on the property that an uninitialised observable multi-trace $\mu =(\sigma _1,\cdots ,\sigma _n)$ is such that each $\sigma _i$ is either empty or of the form , but in the latter case $\mu$ has been obtained from an initialised observable multi-trace of the form $\mu '=(\sigma ''_1,\cdots ,\sigma ''_n)$ where $\sigma ''_i$ is $\varepsilon$ for $\sigma _i = \varepsilon$ and of the form $(d_i,a_i).\sigma '_i$ for . Thus, iff there exist durations $d_1, \cdots , d_n$ where $\mu ''=(\sigma ''_1,\cdots ,\sigma '' _i ,\cdots \sigma ''_n)\in IOTraces(\varLambda )$. We check whether such durations exist by considering them as n variables $d_1, \cdots , d_n$ (of type D); we construct constraints on these variables characterising the properties of observable traces. By definition, only the occurrence of an internal input might break the property. There are two reasons for allowing an initialised observable multi-trace to be extended by an internal input. The first is that a sufficient number of corresponding internal outputs have previously been emitted. The second is that at the time when the extension is performed, the trace emitting the corresponding internal output is no longer observed. If $\sigma _i$ is the trace extended by internal input a, and $\sigma _j$ is the trace at the interface that sends $\overline{a}$, the first case correspond to situation in which $pref(\sigma _j ,\overline{a}, |\rho |_a)$ exists and C: $d_i + dur(\rho ) > d_j + dur\_occ(\sigma _j,\overline{a}, |\rho |_a)$ holds. The latter case corresponds to situations in which $pref(\sigma _j ,\overline{a}, |\rho |_a)$ does not exist and $C'$: $d_i + dur(\rho ) > d_j + dur(\sigma _j)$ holds. However, by definition of $dur\_occ$, when $pref(\sigma _j ,\overline{a}, |\rho |_a)$ does not exist we have that $dur\_occ(\sigma _j,\overline{a}, |\rho |_a)=dur(\sigma _j)$, which means that the constraints C and $C'$ are equivalent. Therefore both cases can be treated in the same way by requiring that C holds, as is done in Algorithm 1. Every new constraint to be considered is added to the set E (line 10). Sat is a function on sets of constraints such that Sat(E) returns True if all constraints in E are simultaneously satisfiable and False otherwise.

5 Experiments

We implemented the approach by separating the verification of local traces (Sect. 4.1) and the verification of the tuple of traces against the definition of observable multi-traces (Definition 6 and Sect. 4.2). If there are n subsystems, the global verdict $Verdict_{g}$ has $n+1$ verdicts $(Verdict_1,\dots ,Verdict_n,Verdict_{com})$ where for l in $[1\ldots n]$, $Verdict_l$ is the local verdict in $\{Pass_l,Fail_l,Inconc_l\}$ associated to the lth component and where $Verdict_{com} \in \{Pass_{com},Fail_{com}\}$ is the verdict relating to the verification of the communication policy.

In order to assess the scalability of the framework, we adopted a mutation-based approach. We first generated multi-traces that are correct by construction with respect to local analyses and communication rules. For this purpose, a global model of the system is built by simulating internal communications using one timed queue per component. Since the reception of a message can be delayed, the model specifies asynchronous communications. Then, we use the symbolic execution platform Diversity⁶ to build long traces, focusing on the behaviours that complete communication scenarios as much as possible. Finally, the resulting multi-traces are directly constructed by considering a tuple made of all projections for each component. Generated multi-traces are then modified by applying some simple mutation schemas. Table 1 summaries mutation schemas we applied on a multi-trace $\mu$ to produce a set of mutated tuples of traces.

Table 1. Mutation schemas on multi-traces

Mutation schemas #1 and #3 require that added or modified events respect syntactic requirements from the system signature and concerning channels and data types. Mutation schema #5 is designed to break the key property of multi-traces, that is that time is necessarily elapsing when messages are transmitted. Let us illustrate with the observable multi-trace $\mu =(\sigma _1,\sigma _2)$ where and . Applying mutation schema #5 consists of breaking the so-called round-trip communication, abbreviated as the acronym RTC, $c_2!v_2\rightarrow c_2?v_2\rightarrow c_3!v_3 \rightarrow c_3?v_3$, for which by construction, the delay between the emission and the reception on the first component has to be strictly greater than the delay between the reception and the emission on the second component. Mutation schema #5 modifies delays between these actions so that there is an internal reception occurring before its corresponding emission is sent. A possible mutation of $\mu$ using mutation schema #5 could be $\mu '=(\sigma '_1,\sigma '_2)$ with and . While the first 4 mutation schemas do not necessarily create faulty multi-traces, mutation schema #5 creates by construction at least a communication fault.

The size of the PhoneX system depends on the number of clients. We consider a system with 3 caller clients, 3 called clients, 3 active sessions and a PhoneX central. In Table 2, the third column (com. checking) give the time⁷ needed to solve the constraint associated to the verification of communications described in a multi-trace whose number of events is given in the first column and number of internal communications is given in the second column. The fourth column provides the time⁸ needed to analyse all local traces. For each multi-trace, we generate 1000 mutated tuples of traces and we count the ratio of multi-traces that are faulty with regards to communication policy (before last column). Finally, in the last column, we give the average time to check the communication constraint of the mutated tuples. Experiments have been performed on a 3.10 Ghz Intel Xeon E5-2687W working station with 64 GB of RAM on Linux Ubuntu 14.04.

Table 2. Experimental data for correct multitraces and their mutants

Among classical solvers, we get best results with the Yices SMT solver [5]. The efficiency of Yices for solving constraints of the form $d_i + x > d_j + y$ where x and y are concrete durations together with the fact that constructing the set of constraints from a tuple is linear explains that communication checking is more efficient than unit testing. Unit testing of subsystems is performed by the extension to unitary testing of the symbolic execution platform Diversity which is coupled with several solvers such as Yices, CVC4 or Z3. Regarding symbolic models without timed issues, functionalities (test case generation driven by test purposes, verdict computation) offered by the Diversity test extension are similar to those provided by the tool STG [4].

6 Related Work

Testing timed distributed systems from models gives rise to several recent works. In [16], hypotheses are broadly the same as those adopted in this paper, namely a model for each local component, and a testing architecture constituted of independent local testers. [16] mainly focuses on the generation of test cases from a global model built by composing local models and queues, similar to the one that we used in Sect. 5. The main difference is that the correction of the system can boil down to the local correction of each component, without any verification of internal communications. In [13], testing of distributed real-time systems is based on the conformance relation tioco and considers timed automata as models. Testers can be local or global so that the testing architecture does not necessarily reflect the one of the system. The authors focus on the construction of analogue-clock and digital-clock test cases. The question of communications is supported by a compositionality result saying that correctness up to tioco is preserved by parallel composition of timed automata provided that they are input-enabled. Similarly, in [22], local testers that can exchange synchronisation messages are derived from a global timed automaton. Thus, all these works are rather interested in the issue of test case generation, assuming testing hypotheses on communications between components, while we leave aside this question to focus on the analysis of traces with almost no hypotheses on internal communications. Lastly, the use of constraint solvers is often advocated when dealing with software and system testing issues [7]. As an example of usage for the verdict computation in MBT, [12] uses SAT solvers for generating checking sequences from finite state machines.

7 Conclusion

We focus on the oracle problem for testing distributed systems against specifications. A system execution is a tuple of timed local traces, one for each location. An observation is correct iff each local trace is allowed by the corresponding specification component and the tuple of local traces defines a valid communication scenario. The oracle problem is reduced to several instances of the standard oracle problem for centralised testing plus a constraint satisfaction problem for communication. This is implemented as an orchestration coordinating several centralised verdict computations using the Diversity tool and calls to classical constraint solvers. We have carried out experiments with a central telecommunication system which have shown low computation time. Our algorithm is designed for active testing in which we run a test and then check the observation made. It would be interesting to extend it to deal with passive testing.