Deriving Interaction Scenarios for Timed Distributed Systems by Symbolic Execution

Abstract

In this paper, we propose a symbolic framework to analyze and debug communicating distributed models. We implement dedicated symbolic execution techniques for such models and use them to compute interaction scenarios satisfying a particular user coverage objective. These scenarios reveal emergent temporal and data correlations that are part of the system specification. To support the understanding and the analysis of such learned knowledge, our tooling allows for an intuitive annotated scenario visualization using sequence diagrams. As an application, we develop behavioral models for the so-called distributed Trickle algorithm which manages information dissemination in Wireless Sensor Networks (WSN). We select relevant scenarios which cover critical communications achieving an up-to-date or outdated state of the network.

1 Introduction

Context and Related Work. Symbolic Execution (SE in short) [10] is a powerful execution technique for analyzing programs or models. Its main principle is to execute a program or a model using variables instead of concrete values. SE collects for each explored path a set of logical constraints on the introduced variables for its execution, called Path Conditions (PC). Therefore, such a symbolic path represents a possibly infinite set of concrete paths. As such, SE is a systematic execution technique, which is valuable for the analysis of complex programs or models. Moreover, SE is gaining interest due to the availability of computing resources and the progress made in constraint solving.

SE has been increasingly used in the analysis of concurrent multi-process systems and more recently of distributed systems. Although we are positioning our work at the level of models of distributed systems, we will discuss related approaches dealing with programs [1, 11, 20, 22, 23, 25] for their relevance and for having addressed early issues related to non-deterministic concurrent executions and/or asynchronous communications. In [1], authors use an object oriented modeling language for programs which allows objects to execute concurrently (or synchronize) and to interact by asynchronous method calls. In [25], the Symbolic PathFinder [21] tool is extended to deal with bytecode of multi-threaded Java programs without communication primitives. Another work [18] still based on PathFinder proposes analysis of inter-process communications. In [11], concrete and symbolic execution are combined to provide an efficient analysis based on a fixed order of scheduling multi-threaded programs. In [22], authors implement SE of distributed systems on top of the KLEE tool [5] by unfolding a number of execution paths for some subsystems while keeping track of their communication history in terms of emitted/received network packets and then identifying pairwise states on packets emitting/recipient subsystems. While combinatorial interleaving is often bypassed by using exploration heuristic or partial order reduction techniques, the originality of this work is to come up with an alternative to interleaved execution of distributed subsystems. SE has been extended to models using variants of abstract labeled transition systems, namely Symbolic Transition Systems (STS in short) [6, 12]. Timed STSs (or TSTS for short) which extend STS with clocks have been defined later in [3, 26, 27]. [26, 27] are rather a merge of Timed Automata [2] and STS so that clock values represent convex abstractions, known as zones, while [3] uses symbolic techniques to homogeneously handle both clocks and other data variables. The DIVERSITY tool [17] implements the SE of TSTS [3, 6] and also provides them with textual syntax and editing features.

Contribution. We adopt a compositional modeling approach based on TSTS like those in [3] for the purpose of modeling behaviors of distributed subsystems. A technical improvement is that we give a new definition of TSTS in which transitions are equipped with an expressive sequential statement language. This statement language mixes computations on clocks and other variables, and enables many steps of communications, guards and variable updates to be combined into a single (symbolic) execution step. The objective is to provide modeling facilities for different levels of detail that may appear in the specification of real distributed systems, such as in the specification of the Trickle case study [13, 14, 16] which has motivated the present work. We then define models of distributed systems as a collection of TSTSs. These are endowed with SE using asynchronous communication mechanisms for which we define time and data interdependencies. More precisely, our SE mechanisms collect all possible information linking data and time on the execution of distributed subsystems. Thus, we propose identification constraints to take into account that values received at a given port necessarily correspond to a value emitted at a port connected to it. Similarly, since a duration between an emission of a message a followed by a reception of a message b at a given location should be greater than the duration between the reception of a followed by the emission of b at a remote location, we consider constraints on delays separating events (emissions/receptions). As part of our contribution, we implement the proposed TSTS-based distributed models together with their SE in the DIVERSITY tool. Interactions between communicating subsystems can therefore be explored in the tool. In order to primarily assess these interaction behaviors, we propose a dedicated selection method that highlights the emissions and their corresponding receptions.

Structure of the Paper. Sect. 2 presents the motivating example of the Trickle-based information dissemination. Section 3 introduces TSTS and their associated SE mechanisms. In Sect. 4, we define TSTS-based models for distributed systems together with dedicated unfolding techniques applying correlated SE of the involved TSTS under asynchronous communication. Then, we show in the section how interaction scenarios can be selected from such models and discuss experimental results on the Trickle case study. Finally, we give some concluding remarks in Sect. 5.

2 Motivating Example: Trickle-Based Dissemination

Trickle [13, 14, 16] is the state-of-the-art distributed algorithm for the dissemination of information across a Wireless Sensors Network (WSN). This algorithm is provided as a standard library in TinyOS [15] and Contiki [8], two of the best known firmware Operating Systems (OS) for WSN. Trickle is also used in recently standardized WSN protocols namely the Multicast Protocol for Low Power and Lossy Networks (MPL) [9] and the Routing Protocol for Low Power and Lossy Networks (RPL) [28]. The dissemination of information across the network is through sensor-to-sensor short-range communications since such small devices can be equipped only with small radio antennas. In addition, such communications may be asymmetric: a node can send messages to another node without the opposite being possible. The network can be seen as a directed graph connecting nodes to their neighbors which can be reached by their transmissions. Trickle is a fully distributed algorithm. Each node applies a set of rules according to its state, i.e., the information it holds. The goal is to converge to an updated global state of the network where all nodes have the same information. The Trickle algorithm can be described as follows:

• each node maintains a current interval $\tau$, a counter c and a broadcasting time t in current interval $\tau$,

• global parameters to all nodes (same values) are k the redundancy constant, $\tau _l$ the smallest value for $\tau$, and $\tau _h$ the largest value for $\tau$,

• each node applies the following rules:

  • 1. at the start of a new interval a node resets its timer and counter c and sets at random t to a value in $[\tau /2,\tau [$,

  • 2. if the node receives a message consistent with the information it holds, it increments c,

  • 3. when its timer reaches t, the node broadcasts a message carrying the information it holds if $c < k$,

  • 4. when its timer expires at $\tau$, it increases its interval length by setting $\tau$ to $\text {min}(2\cdot \tau ,\tau _h)$ and starts a new interval,

  • 5. when a node receives a message that is inconsistent with its own information, then if $\tau > \tau _l$ it sets $\tau$ to $\tau _l$ and starts a new interval, otherwise it does nothing.

Each time an inconsistency is detected, the interval $\tau$ is set to $\tau _l$, then $\tau$ is doubled up to $\tau _h$. Note that the node transmits only if its neighbours are unlikely to be up-to-date, when $c < k$ given c counts receptions of consistent messages in the interval (k is fixed based on neighbours number). If $c \ge k$, the node suppresses the transmission. Moreover, since small intervals are considered immediately after the inconsistency, the frequency of transmissions is greater at the beginning (and decreases when approaching $\tau _h$). This allows nodes to quickly share the same information. Now nodes are not necessarily synchronized, yet Trickle suggests choosing a random t (in $[\tau /2,\tau [$) together with imposing a listen-only period (first half of $\tau$) in order to enhance the distribution of the transmission load between nodes in the interval (and hence energy cost).

Fig. 1.

Illustration of Trickle scenarios

Figure 1 depicts a first scenario (Fig. 1a) between two nodes $node_1$ and $node_2$, each implementing the Trickle algorithm. The second scenario (Fig. 1b) is an abstract scenario that can be obtained by our symbolic execution for which the first scenario is a concretization. The scenarios illustrate the transmission suppress according to Trickle rules, the information being disseminated is a version number. Node $node_1$ emits a version number 0 on its port $node_1.Version$ (denoted by Version!0 on the message with source the axis of $node_1$). This version number is received later by node $node_2$ on its port $node_2.Version$ (denoted by Version?0 on the message with destination the axis of $node_2$). When $node_2$ receives the same version number as it holds, it increments its counter $node_2.c$ which reaches k ($k=1$). This results in suppressing the transmission scheduled at the value stored in $node_2.t$ ($node_2.t=7$) within the second half of the $\tau$-interval ($node_2.\tau =8$). Executions at $node_1$ and $node_2$ are given by the following succession of delays and emissions/receptions:

$node_1:``4,6,6.5,\text {Version}!0"$ and $node_2:``8,7,5.5,\text {Version}?0"$

Initial delays 4 and 8 are measured since a common fictitious time point denoted by 0 on the time axis. They correspond to elapsed time before respectively $node_1$ and $node_2$ are started. The small arrows indicate the start of the nodes on their respective axes. Introducing such delayed initialization is typical for distributed subsystems where there is no global clock. The symbolic scenario encodes such execution using (fresh) variables and logical constraints (Fig. 1c). Constraints $4\le node_1.t_1< 8 \wedge x_2=node_1.t_1$ and $4\le node_2.t_1< 8 \wedge y_2\le node_2.t_1 \wedge node_2.v_1 = node_2.myv_0$ correspond to Path Conditions (PC). On the other hand, constraints $x_0+x_1+x_2\le y_0+y_1+y_2$ and $node_1.myv_0=node_2.v_1$ reflect time and data inter-dependences. Both kind of logical constraints will be inferred by our symbolic execution mechanisms.

3 Models of Timed Symbolic Transition Systems

Preliminaries

A signature is a couple $\varOmega =(S,Op)$ where S is a set of type names and Op is a set of operation names provided with a profile in $S^+$. We denote with $V=\coprod _{s\in S}V_s$ the set of typed variables with ${type}:V\rightarrow S$ the function that associates a variable to its corresponding type. The set of $\varOmega$-terms in V, denoted $\mathcal {T}_{\varOmega }(V)=\coprod _{s\in S}\mathcal {T}_{\varOmega }(V)_{s}$, is inductively defined over V and operations Op of $\varOmega$ as usual and the function type is extended to $\mathcal {T}_{\varOmega }(V)$ as usual. The set of typed equational $\varOmega$-formulas over V, denoted as $\mathcal {F}_{\varOmega }(V)$, is inductively defined over equality predicates $t=t'$ for any $t,t'\in \mathcal {T}_{\varOmega }(V)_{s}$ and over usual boolean connectives. For $\varphi \in \mathcal {F}_{\varOmega }(V)$, we denote $Var(\varphi )\subseteq V$ the set of variables occurring in $\varphi$. A substitution over V is a type-preserving application $\rho : V \rightarrow \mathcal {T}_{\varOmega }(V)$. The identity substitution over V is denoted $id_V$ and the notation $\rho [x \rightarrow t]$ means the substitution identical to $\rho$ except that it associates t with x. Signature $\varOmega$ includes a particular type, denoted $time\in S$, for representing durations, and which is provided with usual operations, i.e., $<:time \times time\rightarrow Bool$ and $+:time \times time\rightarrow time$, ...

An $\varOmega$-model is a set $M=\coprod _{s\in S}M_s$ with $M_s$ a set of values for type s, hence inducing a mapping between each operation name $f:s_1, \dots ,s_{n-1}\rightarrow s_n\in Op$ and the corresponding concrete operation $f_M:M_{s_1}\times \dots \times M_{s_{n-1}}\rightarrow M_{s_n}$. The set $M_{time}$ is denoted D (for the set of durations) and is isomorphic to the set of non-negative real numbers ($\mathbb {R}_{\ge 0}$). An interpretation is an application $\nu : V \rightarrow M$ that associates a value in M to each variable $v\in V$, canonically extended to $\mathcal {T}_{\varOmega }(V)$ and $\mathcal {F}_{\varOmega }(V)$ as usual. For $\nu \in M^V$ and $\varphi \in \mathcal {F}_{\varOmega }(V)$, the satisfaction of $\varphi$ by $\nu$ is denoted $M\models _{\nu }\varphi$ and is inductively defined w.r.t. the structure of $\varphi$ as usual. We say a formula $\varphi \in \mathcal {F}_{\varOmega }(V)$ is satisfiable, denoted $Sat(\varphi )$, if there exists $\nu \in M^V$ such that $M\models _{\nu }\varphi$.

A TSTS-signature is defined as a tuple $\varSigma =(\varOmega ,A,K,P)$, where $\varOmega =(S,Op)$ is a signature, A, K and P are pairwise disjoint sets of variables representing respectively generic data variables (A), clock variables (K) and ports (P). Variables in A and P can take any type in S whereas variables in K (i.e. clocks) are limited to type time. So, each class of variables is partitioned w.r.t. types $s\in S$, hence $A= \coprod _{s\in S}A_s$, $P= \coprod _{s\in S}P_s$ whereas K can be reduced to $K_{{time}}$¹.

As glimpsed in the introduction, transitions of TSTS will be defined using sequential scheduling of statements like in programming languages.

Sequential Statements

A sequential statement (statement in short) stm is defined as follows:

$$\begin{array}{ll} stm :\,:= &{} \mathbf{skip}~|~p\mathbf{?}x~|~p\mathbf{!}t_1~|~x\mathbf{:=} t_2 ~|~\mathbf{newfresh}(x)~|~\mathbf{\big [}\phi \mathbf{\big ]} ~|~ \\ &{} stm_1 \mathbf{;} stm_2~|~ \mathbf{if} \mathbf{\big (} \phi \mathbf{\big )}\, \mathbf{then}\,stm_1\,\mathbf{else}\, stm_2 \end{array}$$

with $p\in P$, $x\in A\cup K$, $t_1\in \mathcal{T}_\varOmega (A \cup K)_{type(p)}$, $t_2\in \mathcal{T}_\varOmega (A \cup K)_{type(x)}$, and $\phi \in \mathcal {F}_{\varOmega }(A\cup K)$. The set of statements over $\varSigma$ is denoted by $Stm(\varSigma )$.

$\mathbf{skip}$ is the null statement; p?x denotes the reception, on port p, of a value which is stored in x, whereas $p!t_1$ denotes the emission, on port p, of the value corresponding to the current interpretation of term $t_1$; $x:=t_2$ assigns the variable x with a new value denoted by $t_2$; $\mathbf{newfresh}(x)$ randomly assigns x with a new value; $\big [\phi \big ]$ denotes a condition on variables which enables the statement execution. Moreover, statements can be built using sequence ($\mathbf{;}$) and condition ($\mathbf{if} \ldots \mathbf{then} \ldots \mathbf{else} \ldots$).

Timed Symbolic Transition Systems (TSTS)

A TSTS over a TSTS-signature $\varSigma =(\varOmega ,A,K,P)$ is a triple $\mathbb {G}=(Q,q_0,{Tr})$, where Q is the set of states, $q_0\in Q$ is the initial state and Tr is the set of transitions of the form $(q,stm,q')$ with $q, q'\in Q$, and $stm\in Stm(\varSigma )$.

For a transition $tr=(q,stm,q')$, q (resp. $q'$) is the source (resp. target) state of the transition. stm is called the statement of the transition. We use the notations src(tr), tgt(tr) and stm(tr) to refer to q, $q'$ and stm respectively. For $\mathbb {G}=(Q, q_0, {Tr})$ a TSTS, we use $States(\mathbb {G})$, $initSt(\mathbb {G})$ and ${Trans}(\mathbb {G})$ to respectively refer to Q, $q_0$ and Tr.

Fig. 2.

Timed Symbolic Transition Systems (TSTS) modeling a Trickle node

Figure 2 depicts a TSTS which models the behavior of a Trickle node, according to rules described in Sect. 2.

From the initial state $q_0$, the node assigns t with a new fresh value using the action ${\mathbf{newfresh}}(t)$, this new value for t is constrained by the guard $[\tau /2 \le t < \tau ]$. The clock² cl is initially reset, as glimpsed before it is used to activate the different Trickle events, that is when reaching t and starting new $\tau$-intervals.

When node reaches the state $q_1$, it can receive a message (on port $\text {Version}$) from a neighboring node before reaching t (loop-transitions on $q_1$). Such message carries a version number. The message is processed as follows (see macro $\text {updateVersion}$): if the node is outdated, it updates its version number ($myv:=v$). Trickle rule related to (in)consistency is then applied: if the neighbour is up-to-date, i.e., the node and its neighbour agree the version number, then the counter c of the node is incremented; otherwise a new $\tau$-interval is considered for the node where $\tau$ and c are reset, since additional little-spaced messages are needed for convergence. When $cl=t$, the transmission is scheduled only if $c < k$ in order to inform neighbors of version number the node possesses (horizontal transition $q_1\rightarrow q_2$), otherwise the process does nothing (curved transition $q_1\rightarrow q_2$).

At the state $q_2$, while $cl \le \tau$ and messages are consistent (agree on version number), the counter c is incremented (loop-transition on $q_2$), upon the reception of inconsistent message (different version number) the node starts a new $\tau$-interval by resetting both cl and c (upper transition $q_2\rightarrow q_1$). When $cl = \tau$, the node increases the listening interval by doubling $\tau$ (up to $\tau _h$) (lower transition $q_2\rightarrow q_1$).

Symbolic Execution of TSTS

Given a TSTS signature $\varSigma =(\varOmega ,A,K,P)$, we introduce a set of so-called fresh variables (also called symbolic parameters) $F=\bigcup _{s \in S}F_{s}$ which is disjoint from both the data and clock variables of $\varSigma$ (i.e. $F\cap (A\cup K) = \emptyset$). We write $F_{t}\subseteq F$ for the set of fresh variables of type time and $F_{d}=F\backslash F_{t}$ for the set of non-time fresh variables. In the following, we will refer to the signature $\varSigma _F=(\varOmega ,F,\emptyset ,P)$ to define the symbolic execution of a TSTS which is defined over $\varSigma$.

Execution contexts (EC in short) are data structures used to store information characterizing logical constraints on symbols related to an actual execution of a TSTS. An EC of a TSTS $\mathbb {G}=(Q, q_0, {Tr})$ is a tuple $ec=(q,\pi ,\lambda ,\theta ,Act,pec)$:

• $q \in Q$ is the (current) state of $\mathbb {G}$,

• $\pi \in \mathcal {F}_{\varOmega }(F)$ is a constraint that should be satisfiable in order to reach ec.

• $\lambda :A\cup K \rightarrow \mathcal {T}_{\varOmega }(F)$ is a type-preserving substitution through which data variables of $\mathbb {G}$ are replaced by terms over variables in F,

• $\theta \in \mathcal {T}_{\varOmega }(F_t)$ is a term denoting the sum of durations elapsed so-far since the beginning of the execution of $\mathbb {G}$,

• Act is a sequence of emissions and/or receptions that have occurred since the beginning (; ;  stands for the empty sequence),

• and pec is the parent EC which allowed ec to be reached.

We distinguish initial execution contexts of the form $ec_0=(q_0,true,\lambda _0,z_0,;;,self)$ such that $\lambda _0$ associates to each variable of $A \cup K$ a fresh variable in F verifying $\forall \theta \in K$, $\lambda _0(\theta )=z_0$ and $\forall x\ne y \in A$, $\lambda _0(x)\ne \lambda _0(y)$ and $\lambda _0(x)\ne z_0$."self" is a special identifier indicating that by convention, the parent EC of an initial execution $ec_0$ is itself. $Var(ec_0) \subseteq F$ is the set of all fresh variables occuring in $ec_0$. To refer to the constituents of an EC $ec=(q,\pi ,\lambda ,\theta ,Act,pec)$, q(ec) stands for q, $\pi (ec)$ for $\pi$, $\lambda (ec)$ for $\lambda$, $\theta (ec)$ for $\theta$, Act(ec) for Act and pec(ec) for pec. We denote $\mathcal {EC}(\mathbb {G})$ ($\mathcal {EC}_0(\mathbb {G})$) the set of all (initial) execution contexts ec of $\mathbb {G}$ such that we have $Sat(\pi (ec))$. In order to take advantage that only some components of an EC are likely to be modified at each symbolic execution step, we will use a kind of additive notation which will point out the only modified components of ECs: for example, with ec an EC, $ec' = ec[Act \rightarrow Act;act]$ means that $ec'$ coincides with ec except that the component $Act(ec')$ is Act(ec); act.

Symbolic Execution of Statements

Let stm and $\mathbb {G}$ be resp. a statement and a TSTS both defined over $\varSigma$ and let $ec \in \mathcal {EC}(\mathbb {G})$. The set $SE(stm)_{ec} \subseteq \mathcal {EC}(\mathbb {G})$ of ECs reached from ec by symbolic execution of stm is defined as follows:

$$\begin{aligned} SE(\mathbf{skip})_{ec} =\{ec\}&\end{aligned}$$

(1)

$$\begin{aligned} SE(p?x)_{ec} =\{ec[\lambda \rightarrow \lambda [x \rightarrow y],Act \rightarrow Act;p?y]\}&\ \ \ y \in F_{type(x)} \end{aligned}$$

(2)

$$\begin{aligned} SE(\mathbf{newfresh}(x))_{ec} =\{ec[\lambda \rightarrow \lambda [x \rightarrow y]] \}&\ \ \ y \in F_{type(x)}\end{aligned}$$

(3)

$$\begin{aligned} SE(p!t_1)_{ec} = \{ec[Act \rightarrow Act;p!\lambda (t_1)]\}&\end{aligned}$$

(4)

$$\begin{aligned} SE(x:= t_2)_{ec} = \{ec[\lambda \rightarrow \lambda [x \rightarrow \lambda (t_2)]] \}&\end{aligned}$$

(5)

$$\begin{aligned} SE(\big [\phi \big ])_{ec}=\{ec[\pi \rightarrow \pi \wedge \lambda (\phi )] \}&\end{aligned}$$

(6)

$$\begin{aligned} SE(stm_1;stm_2)_{ec}=\bigcup _{ec'_0 \in SE(stm_1)_{ec}} SE(stm_2)_{ec'_0}&\end{aligned}$$

(7)

$$\begin{aligned} SE(\mathbf{if}\big (\phi \big )\mathbf{then}\,stm_1\,\mathbf{else}\, stm_2)_{ec}= SE(stm_1)_{ec[\pi \rightarrow \pi \wedge \lambda (\phi )]}&\\ \cup SE(stm_2)_{ec[\pi \rightarrow \pi \wedge \lambda (\lnot (\phi ))]}&\nonumber \end{aligned}$$

(8)

Symbolic Execution of Transitions

Let $tr=(q,stm,q')$ be a transition of $\mathbb {G}$ and $ec=(q,\pi ,\lambda ,\theta ,Act,ec)$ be an EC of $\mathcal{EC}(\mathbb {G})$. The set of ECs $SE(tr)_{ec}$ reached from ec by symbolic execution of tr is defined as the set of all $ec'=(q',\pi ',\lambda ',\theta +z,Act',ec)$ such that there exists $(q,\pi ',\lambda ',\theta ,Act',pec)$ in $SE(stm(tr))_{ec[\lambda \rightarrow \lambda '_0]}$ where $\lambda '_0$ is defined as follows:

$$\begin{aligned} \lambda '_0(w) = \lambda (w)+z \ \mathbf{for}\ w \in K \ \ \mathbf{and}\ \ \lambda '_0(w) = \lambda (w) \ \mathbf{for} \ w \in A \end{aligned}$$

(9)

with z a fresh variable in $F_t$, denoted as $delay(ec')$ in the sequel.

The set of ECs $ec'$ reached from of a given EC ec by executing $tr\in Trans(\mathbb {G})$ is obtained in two steps. First, all clocks are increased by the same amount of time, denoted by the time-typed variable $z\in F_t$ which allows to obtain the intermediate substitution $\lambda '_0$ (9). Second, transition statement stm(tr) is evaluated from the newly built context, i.e., ec in which $\lambda '_0$ replaces $\lambda$. ECs obtained then, characterize substitutions $\lambda '$ reflecting data variables substitutions by new variables as defined by the statement symbolic execution.

Symbolic Execution of TSTS

The symbolic execution of a TSTS $\mathbb {G}$ from $ec_0\in \mathcal{EC}_0(\mathbb {G})$ is the smallest set of ECs, denoted as $SE(\mathbb {G})_{ec_0}$, satisfying: $ec_0\in SE(\mathbb {G})_{ec_0}$ and for any $tr\in Trans(\mathbb {G})$, $ec \in SE(\mathbb {G})_{ec_0}$ such that $q(ec)=src(tr)$, we have $SE(tr)_{ec}\subseteq SE(\mathbb {G})_{ec_0}$. This results in a tree structure en-rooted in $ec_0$.

4 Distributed Models and Interaction Scenarios Derivation

We use TSTS to specify Timed Distributed Systems (DS in short). A remote subsystem is characterized by a TSTS. Communications between subsystems TSTSs are specified by asynchronous data-passing over unbounded fifo queues.

Distributed System Model

A Distributed System model $Sys=(\mathbb {G}_1,\cdots ,\mathbb {G}_m,\varGamma )$ is defined by:

• a family $(\mathbb {G}_i)_{i \in \{1,..m\}}$ of TSTS defined over $\varSigma _i=(\varOmega ,A_i,K_i, P_i)$ verifying that different sub-systems do not share constituents, i.e., $\forall i,j\le m$ with $i\ne j$, $A_i\cap A_j= \emptyset$, $K_i \cap K_j =\emptyset$ and $P_i \cap P_j =\emptyset$,

• the function $\varGamma :P_{Sys} \rightarrow 2^{P_{Sys} }$ specifying connections between ports.

The set of all ports of Sys is denoted by $P_{Sys}=\bigcup _{i\le m} P_i$. Besides, the set of all generic data variables (resp. clock variables) of Sys is denoted by $A_{Sys}=\bigcup _{i\le m} A_i$ (resp. $K_{Sys}=\bigcup _{i\le m} K_i$).

From now on, Sys will denote a generic DS model. We now define the symbolic execution of Sys over the signature $\varSigma ^{Sys}_F=(\varOmega ,F,\emptyset ,P_{Sys})$. Figure 3 depicts a DS for a grid topology of four Trickle nodes, each is associated with a TSTS.

Fig. 3.

Distributed System for a Trickle grid topology

System Execution Context. A system execution context (or a SC) of Sys is a tuple $ec_{sys}=(ec_1,\cdots ,ec_m,\gamma ,\chi ,pec_{sys})$ where

• $ec_i \in \mathcal {EC}(\mathbb {G}_i)$ with $i\le m$, is an EC over $\varSigma ^{Sys}_F$,

• $\gamma : P_{Sys} \rightarrow (\mathcal {T}_{\varOmega }(F_{d})\times \mathcal {T}_{\varOmega }(F_{t}))^*$,

• $\chi \in \mathcal {F}_{\varOmega }(F)$,

• and $pec_{sys}$ is either the identifier self or any other SC.

$\mathcal {EC}(Sys)$ is the set of all SC of Sys and we can access to components of $ec_{sys}$ using notations $\gamma (ec_{sys})$,$\chi (ec_{sys})$ or $pec_{sys}(ec_{sys})$.

$\gamma$ associates to each port the content of its fifo queue in terms of a received piece of data and its emission date. $\chi$ represents a constraint on time and data inferred from data exchanges in Sys. As in the unitary case, $pec_{sys}$ gives access to the SC from which $ec_{sys}$ has been built. Similarly, if $pec_{sys} = self$, $ec_{sys}$ is then an initial SC. The symbolic execution of a DS-model consists in executing a transition of one of its component TSTS $\mathbb {G}_i$ and making execution contexts of Sys evolve accordingly. Intuitively, the evolution of the overall SC will essentially concern the EC relating to the TSTS $\mathbb {G}_i$ for which the transition is being executed.

Symbolic Execution of Transition in a DS-Model

For a SC $ec_{sys}=(ec_1,\cdots ,ec_i,\cdots , ec_m,\gamma ,\chi ,pec_{sys})$, let tr be a transition in $\mathbb {G}_i$ such that $i\le m$ and $src(tr)=q(ec_i)$. The symbolic execution $SE(tr)_{ec_{sys}}$ of tr from $ec_{sys}$ is the set of $ec'_{sys}=(ec'_1,\cdots ,ec'_i,\cdots ,\gamma ',\chi ',ec_{sys})$ provided that all components of $ec'$ are well defined according to the rules:

• $ec'_i \in SE(tr)_{ec_i}$

• for all $j\le m$ such that $j\ne i$, $ec'_j=ec_j$

• $(\gamma ',\chi ')= SE(Act(ec'_i))_{(\gamma ,\chi )}$ with $SE(Act)_{(\gamma ,\chi )}$ inductively defined or undefined as follows:

  • for Act the empty sequence ($Act = ;;$), $(\gamma ,\chi )$

  • for Act of the form $p!t;Act'$, $SE(Act')_{(\gamma [ q \rightarrow \gamma (q).(t,\theta (ec'_i)) ]_{q \in \varGamma (p)},\chi )}$

  • for Act of the form $p?x;Act'$ s.t. there exists a port q verifying $p \in \varGamma (q)$,

    • $SE(Act')_{(\gamma [ p \rightarrow w],\chi \wedge (\theta (ec'_i) \ge \theta ) \wedge (x=t))}$ if $\gamma (p)$ is of form $(t,\theta ).w$

    • undefined if $\gamma (p) = \epsilon$ (i.e. $\gamma (p)$ is an empty fifo queue)

  • for Act of the form $p?x;Act'$ s.t. for all ports q, $p \not \in \varGamma (q)$, $SE(Act')_{(\gamma ,\chi )}$.

When $ec'_{sys}$ is defined, $ec(ec'_{sys})$ denotes $ec'_i$ the execution context directly modified by the last executed transition ($tr \in Tr(\mathbb {G}_i)$). In a nutshell, an emission on a port p has the effect of filling all the fifo associated to the ports of $\varGamma (p)$ and the reception of a message on port p consumes the first message stored in its fifo. Simultaneously, all the knowledge about data and durations are translated into constraints. Let us note that for a transition tr carrying a reception on a port p connected to a port of other subsystems ($p \in \varGamma (q)$ for some q), if its fifo is empty ($\gamma (p)=\epsilon$), then $SE(tr)_{ec_{sys}}$ is undefined so that tr cannot be executed in the current SC.

Symbolic Execution of a DS-Model

Let us introduce $ec^0_{sys}$ an initial SC defined as a tuple $(ec^1_0,\cdots , ec^{m}_0,\gamma _0,true,self)$ where for all $i\le m$, $ec^i_0$ is in $\mathcal {EC}_0(\mathbb {G}_i)$ and for all p in $P_{Sys}$, $\gamma _0(p)$ is the empty queue, i.e. is $\epsilon$. The symbolic execution $SE(Sys)_{ec^0_{sys}}$ of Sys is the smallest set of SC containing $ec^0_{sys}$ and all SC reached by symbolic executions of any $tr\in \bigcup _{i\le m} Trans(\mathbb {G}_i)$ from any $ec_{sys}\in SE(Sys)_{ec^0_{sys}}$. A system symbolic path $pa_{sys}$ is a sequence $ec^0_{sys} ec^1_{sys}\ldots ec^k_{sys}$ such that for all $0< i < k$, $pec_{sys}(ec^{i+1}_{sys}) = ec^{i}_{sys}$, we denote $tgt(pa_{sys})=ec^k_{sys}$, the target of $pa_{sys}$.

For any $ec_{sys}=(ec_1,\cdots ,ec_m,\gamma ,\chi ,pec_{sys})$, we note $\pi (ec_{sys})=(\bigwedge _{i \le k} \pi (ec_i)) \bigwedge \chi$.

A symbolic path $pa_{sys}$ is feasible iff $Sat(\pi (tgt(pa_{sys})))$.

Selection Method

Interaction scenarios will be selected based on the computation of a feasible path $pa_{sys}$ from the symbolic execution tree of the overall DS model Sys. The method favors the selection of system paths with a high coverage of subsystems pairwise Emissions (E) and Receptions (R) in the spirit of the work [24] and that of our previous experimental work on Trickle [4, 19]. The idea is to guide the SE of Sys with the objective to compute a system path $pa_{sys}$ which covers sequences where an emission (p!a) of a piece of data a by some subsystem is followed by the corresponding reception (q?a) of a by another subsystem ($q\in \varGamma (p)$). The selection is implemented according to the Send Receive Pair Coverage criterion (SRPC) [24] by defining coverage sequences based on internal pairwise Emissions and Receptions. To cope with the potential combinatorial explosion due to asynchrony, we have integrated the SRPC criterion with some exploration heuristics available in the tool DIVERSITY [17].

Table 1. Experimentation for Trickle

Experimentation. Table 1 gives some metrics on symbolic exploration for the computation of updated/outdated scenarios on grid topologies T1 (Fig. 3) and T2 (T2 has a connection less). The results are obtained on a PC equipped with an Intel Core i7 processor and 32GB RAM. The outdated scenario given in Fig. 4 is the one described on line 5 of Table 1. We report on the size of all other generated scenarios in terms of number of Emissions and Receptions. We have used CVC4 solver to check the feasibility of logical constraints inferred for scenarios (system paths). We report on BFS (Breadth-First Search) in order to illustrate the exploration combinatorial. Even though left running for more than one hour, only partial coverage has been achieved with BFS. Then we have evaluated the coverage under the heuristic. Experiments show reduced running time. Given the overall short running time of our selection mechanism on the 4 asynchronous Trickle nodes, we expect it to be scalable to many other nodes. The reader can refer to [7, 29, 30] for some informative running time results on model-checking other Trickle case studies, yet in synchronous setting. Those first results need to be consolidated with further experiments.

Fig. 4.

A Trickle scenario for the topology of Fig. 3

Figure 4 depicts a sequence diagram of $node_4$ being outdated for some duration since the start of new version dissemination held by $node_1$ (Topology T1). The diagram has been adapted from the output generated by DIVERSITY. Neighbors of $node_4$, that are $node_2$ and $node_3$ are first updated by $node_1$ with a new version (green messages), they hence reset their interval to $\tau _l$. After that, $node_4$ sends its version (old with respect of that of $node_1$) and gets them to reset their interval (blue messages). Thus, the transmissions of $node_2$ and $node_3$ are postponed; this gives time to $node_1$ re-transmit its version again and saturate their counters (orange messages); therefore they suppress their transmissions for $node_4$ respectively at $y_4+y_5=node_2.t_3$ and $z_4+z_5=node_3.t_3$ (last logical constraints in the scenario). Beyond highlighting such atypical scenarios, the symbolic execution of the model has allowed us to better understand the complex concurrency between nodes, which are ruled by non-trivial time constraints.

5 Conclusion

We have provided a symbolic execution framework for timed distributed models fitted with feasible scenario selection mechanisms. Our framework has been completely implemented in the DIVERSITY tool and applied successfully on the distributed Trickle case study models using a heuristic approach. We believe that efficient novel partial order reduction techniques under the time setting -that we plan to develop in the near future- can leverage on this selection mechanism in order to accelerate the targeted selection for wide Trickle topologies.