# Revisiting semantics of interactions for trace validity analysis

Erwan Mahe, Christophe Gaston, Pascale Le Gall

► To cite this version:

Erwan Mahe, Christophe Gaston, Pascale Le Gall. Revisiting semantics of interactions for trace validity analysis. Lecture Notes in Computer Science, 2020, 12076, pp.482-501. 10.1007/978-3-030-45234-6_24. cea-04224596

HAL Id: cea-04224596

https://cea.hal.science/cea-04224596

Submitted on 2 Oct 2023

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
# Revisiting Semantics of Interactions for Trace Validity Analysis

Erwan Mahe<fnref n="1" />, Christophe Gaston<fnref n="2" />, and Pascale Le Gall<fnref n="1" />

**Abstract.** Interaction languages such as MSC are often associated with formal semantics by means of translations into distinct behavioral formalisms such as automatas or Petri nets. In contrast to translational approaches we propose an operational approach. Its principle is to identify which elementary communication actions can be immediately executed, and then to compute, for every such action, a new interaction representing the possible continuations to its execution. We also define an algorithm for checking the validity of execution traces (i.e. whether or not they belong to an interaction's semantics). Algorithms for semantic computation and trace validity are analyzed by means of experiments.

**Keywords:** Interaction Language · Scenario · Sequence Diagram · Semantics · Causal Order · Trace Analysis

## 1 Introduction

Interaction Languages (IL) are powerful mechanisms to express behavioral requirements in the form of scenarios called *interactions*. ILs include several recognized standards such as MSC and LSC [6], HMSC [25], MSD [13], UML-Sequence Diagrams [21] (UML-SD), etc. These graphical languages represent parts involved in a communication scheme as vertical lines, called lifelines. Each one highlights a succession of instants where actions (emissions or receptions of messages) may occur. These instants are conventionally ordered from top to bottom as illustrated (in the style of UML-SD) in Fig.1-a, where the emission of $m_1$ occurs before that of $m_2$. However, this sequencing does not order actions occurring on different lifelines; in Fig.1-b, even though the reception of *m* occurs graphically below the emission of *m*, no order is enforced. As such, this specificity is called 'weak sequencing'. In order to enforce a causality relation between such uncorrelated actions, we

<figure><img src="image_2.png" /><figcaption>Fig. 1: UML-SD style</figcaption></figure>

<footnote n="1">¹ Laboratoire de Mathématiques et Informatique pour la Complexité et les Systèmes CentraleSupélec - Plateau de Moulon
9 rue Joliot-Curie, F-91192 Gif-sur-Yvette Cedex</footnote>

<footnote n="2">² CEA, LIST, Laboratory of Systems Requirements and Conformity Engineering, P.C. 174, Gif-sur-Yvette, 91191, France</footnote>
use a different 'strict sequencing' operator. In Fig. 1-c, it is used to express a message *m* passing between lifelines *a* and *b*. Here, *m* cannot be received before being emitted; the origin of the arrow denoting an instant preceding the one depicted by its target. Additional operators (e.g. UML-SD combined fragments) enable the expression of various concepts to order actions such as parallelisation, repetition, alternatives (illustrated in Fig. 2), etc. They structure interactions and specify relative scheduling for subscenarii.

<figure><img src="image_3.png" /><figcaption>Fig. 2: Syntax and Positions</figcaption></figure>

When ILs are fitted with formal semantics, requirements can be processed using formal techniques, such as model-checking [1] or model-based testing [19]. As pointed out earlier, the key semantic concept here is the causality relation between actions that the interaction's structure induce. Valid traces are those respecting the subsequent partial order [27,19]. The authors of [17] define a simple IL as a set of terms built above basic actions and provide it with a denotational semantics which associates each

interaction term with a set of traces. This kind of formal framework can serve as a reference for stating theorems about interactions (e.g. the 'satisfaction condition' proven in [17]).

In this paper, we consider an IL which includes several distinct *loop* operators and provide it with a denotational semantics, directly comparable to that given by [17]. The semantics of an interaction with *loops* is defined by considering any finite number of loop unfolding combinations. Then, we introduce a second semantic, which can be qualified as operational, as we aim at presenting it in the style advocated in [24]. Here, accepted traces of an interaction *i* are defined by identifying its initial actions *act*, and for each of those the subsequent interaction *i'* that will express the remainder of the trace. This operational semantics can therefore be thought of as a set of rules of the form *i* $\xrightarrow{act}$ *i'*. Doing so is however challenging as we need to keep track of possible conflicts between actions occurring on the same lifeline. While the operational semantics is particularly suitable to be adapted into concrete trace analysis algorithms, the denotational semantics serves as a mathematical foundation, revealing interesting algebraic properties. Both semantics have been implemented for semantic computation and conducted experiments indicate identical results. A trace analysis tool has also been adapted from the operational semantics and experimented on for correctness and performances.

The paper is organized as follows: Sec. 2 introduces the IL and the denotational semantics. Sec. 3 and Sec. 5 resp. introduce the operational semantics and the subsequent trace analysis algorithm while Sec. 4 reports experimental results about the consistency of both semantics w.r.t. one another. Finally, Sec. 6 and Sec. 7 resp. discuss related works and provide concluding remarks.
# 2 Interaction language and denotational semantics

## 2.1 Base syntax

This section provides a textual denotation of our basic IL (i.e. without loops). Interactions are defined up to a given signature $(L, M)$ where $L$ and $M$ resp. are sets of lifelines and messages. Their base building blocks are a set of communication actions (actions) over $L$ and $M$: $Act(L, M) = \{l\Delta m|l \in L, \Delta \in \{!, ?\}, m \in M\}$ where $l!m$ (resp. $l?m$) designates the emission (resp. reception) of the message $m$ from (resp. on) the lifeline $l$. For any action $act$ in $Act(L, M)$ of the form $l\Delta m$, $\theta(act)$ denotes the lifeline $l$. Actions can be composed using different binary operators that introduce an order of execution between them (weak or strict sequentiality, parallelism, mutual exclusivity).

**Definition 1 (Basic Interactions).** The set $\mathbb{B}(L, M)$ of basic interactions over $L$ and $M$ is inductively defined as follows:

$$ - \emptyset \in \mathbb{B}(L, M) \text{ and } Act(L, M) \subset \mathbb{B}(L, M), $$

$$ - \forall (i_1, i_2) \in \mathbb{B}(L, M)^2 \text{ and } \forall f \in \{\text{strict}, \text{seq}, \text{alt}, \text{par}\}, f(i_1, i_2) \in \mathbb{B}(L, M). $$

The empty interaction $\emptyset$ and actions of $Act(L, M)$ are elementary interactions. The strict and seq operators are sequential operators: in strict$(i_1, i_2)$, all the actions in $i_1$ must take place before any action in $i_2$ while in seq$(i_1, i_2)$ sequentiality is only enforced between actions that share the same lifeline. In Fig.1-b, $b?!m$ may precede$^3$ $a!m$ (because $a \neq b$) while in Fig.1-c $b?!m$ cannot precedes $a!m$. Hence we use strict to encode the emission and reception of the same message object e.g. strict($a!m, b?!m$) on Fig.1-c$^4$. In alt$(i_1, i_2)$, the behaviors specified by $i_1$ and $i_2$ are both acceptable albeit mutually exclusive$^5$. In Fig.2 if $a!m_1$ happens then $b?!m_2$ cannot happen and vice-versa. In par$(i_1, i_2)$, the executions of $i_1$ and $i_2$ are interleaved. For instance, in par($a!m_1, a!m_2$), actions $a!m_1$ and $a!m_2$ can happen in any order.

Interactions being defined as usual terms, we use positions expressed in Dewey decimal notation to refer to subinteractions [7]. A position $p$ of $i$ is a sequence of positive integers denoting a path leading from the root node of $i$ to the subterm of $i$ at position $p$. Interactions are defined with operations whose arity is at most 2. Hence, positions are words of $\{1, 2\}^*$ i.e. words built over the empty word $\epsilon$, the words 1 and 2 and the concatenation law ".". In the following, we will use simplified notations without dots, e.g. "11" for the position "1.1".

In Def.2, the functions $ST$ and $pos$ resp. associate to any interaction the set of all its subinteractions and the set of its positions. Moreover, we use the usual notation $i|_p$ [7] to designate unambiguously the subinteraction of $i$ at position $p$ for $p \in pos(i)$ (cf. example in Fig.2).

<footnote>$^3$ Note that we omit depicting seq on diagrams as is classically done in UML-SD.</footnote>

<footnote>$^4$ drawn by convention as a plain arrow between a and b</footnote>

<footnote>$^5$ note that we handle the UML-SD opt operator as $opt(i) = alt(i, \emptyset) = alt(\emptyset, i)$</footnote>
**Definition 2 (Positions and subinteractions of a basic interaction).** We define $ST : \mathbb{B}(L, M) \to \mathcal{P}(\mathbb{B}(L, M))$, $pos : \mathbb{B}(L, M) \to \mathcal{P}(\{1, 2\}^*)$ and$^{6}_{|-}$ : $\mathbb{B}(L, M) \times \{1, 2\}^* \to \mathbb{B}(L, M)$ such that $\forall i \in \mathbb{B}(L, M):$

- if $i = \emptyset$ or $i \in Act(L, M)$ then $ST(i) = \{i\}$, $pos(i) = \{\epsilon\}$ and $i|_{\epsilon} = i$

- if $i = f(i_1, i_2)$ with $f \in \{\text{strict, seq, par, alt}\}$ then:

• $ST(i) = \{i\} \cup ST(i_1) \cup ST(i_2)$

• $pos(i) = \{\epsilon\} \cup 1.pos(i_1) \cup 2.pos(i_2)$

• $i|_{\epsilon} = i$ and for $p = 1.p'$ (resp. $2.p'$) in $pos(i)$, $i|_{p} = i_{1|p'}$ (resp. $i_{2|p'}$).

## 2.2 Denotational semantics for basic interactions

As explained in Sec.2.1, operators occurring in an interaction induce relations of precedence between the actions of the interaction. In the example of Fig.2, if the left branch of the *alt* is chosen (i.e. $a!m_1$ at position 11) then the action $a!m_3$ at position 2 must occur after it. However if the other branch were chosen (i.e. $b?m_2$ at position 12), there would be no precedence order between actions $b?m_2$ and $a!m_3$ as their common ancestor is a *seq* operator which only orders actions sharing the same lifeline. As a result, several orderings can be defined, depending, among others, on the choice of *alt* branches. These possible orderings can be encoded as a set $ord(i)$ (defined in Def.4) which contains elements of the form $(e, o)$ where $e$ is the set of positions of the involved actions and $o$ reflects the precedence relations between those. In the example of Fig.2, we have $ord(i) = \{({11, 2}), ({11, 2})\}, ({12, 2}), \emptyset\}$. Indeed, as explained earlier, if the 11 branch is chosen then the only two actions to be considered are $a!m_1$ and $a!m_3$ on resp. positions 11 and 2 (therefore $e = \{11, 2\}$) and they are ordered because of both the *seq* operator and their common lifeline, so that the associated precedence relation is modelled by $o = \{({11, 2})\}$ meaning that $a!m_1$ at position 11 should occur before $a!m_3$ at position 2. The only other possible ordering occurs when branch 12 is chosen and likewise we would have $e = \{12, 2\}$ with $o = \emptyset$ because the *seq* does not constrain the order of actions $b?m_2$ and $a!m_3$ with different lifelines.

**Definition 3 (Ordering type).** Given $i$ in $\mathbb{B}(L, M)$. The set $\mathcal{O}(i)$ of candidate orderings of $i$ contains all couples $(e, o)$ such that (**1**) $e \subseteq pos(i)$, (**2**) for any $p$ in $e$, $i|_p \in Act(L, M)$ and (**3**) $o \subseteq e \times e$. $\mathcal{O}$ is then the set $\bigcup_{i \in \mathbb{B}(L, M)} \mathcal{O}(i)$.

In Def.4, for a given interaction $i$, $ord(i)$ precisely defines which orderings are to be considered among the candidate orderings $\mathcal{O}(i)$. For an ordering $(e, o)$ in $\mathcal{O}$ and $p \in \{1, 2\}$, we use the notation $p.e = \{p.p'|p' \in e\}$, $p.o = \{(p.p_1, p.p_2)|(p_1, p_2) \in o\}$ and $p.(e, o) = (p.e, p.o)$. The notation is canonically extended to any set $O$ of orderings, by $p.O = \{p.(e, o)|(e, o) \in O\}$.

For the interaction $\emptyset$, there is no associated action and therefore we have a single $(e, o) = (\emptyset, \emptyset)$. For $a \in Act(L, M)$, there is a single action $a$ (at position $\epsilon$) and as a result, $ord(a)$ contains a single $(e, o) = (\{\epsilon\}, \emptyset)$. For $i = alt(i_1, i_2)$,

<footnote>$^{6}_{|-}$ is a partial function so that $i|_p$ is only defined for positions occurring in $pos(i)$.</footnote>
either $i_1$ or $i_2$ is executed. Thus any ordering in $ord(i)$ is simply an ordering from $ord(i_1)$ or from $ord(i_2)$ but correctly prefixed. Concretely, for any orderings $(e_1, o_1) \in ord(i_1)$ and $(e_2, o_2) \in ord(i_2)$, $ord(i)$ contains both $1.(e_1, o_1)$ and $2.(e_2, o_2)$. For $i = par(i_1, i_2)$, both $i_1$ and $i_2$ have to be executed but no order is enforced between actions of either child branch. Thus, for any ordering $(e_1, o_1) \in ord(i_1)$ and $(e_2, o_2) \in ord(i_2)$, $ord(i)$ contains $(1.e_1 \cup 2.e_2, 1.o_1 \cup 2.o_2)$. For $i = strict(i_1, i_2)$ both $i_1$ and $i_2$ have to be executed and all actions from $i_1$ must occur before actions from $i_2$. Thus for any orderings $(e_1, o_1) \in ord(i_1)$ and $(e_2, o_2) \in ord(i_2)$, $ord(i)$ contains an ordering $(e, o)$ that concerns all actions from both children i.e. $e = 1.e_1 \cup 2.e_2$ and such that $o$ keeps track of all initial precedence relations while incorporating those induced by the strict operator i.e. $o = 1.o_1 \cup 2.o_2 \cup \{(p_1, p_2)|p_1 \in 1.e_1, p_2 \in 2.e_2\}$. For $i = seq(i_1, i_2)$ the same reasoning can be applied, with the exception that additional precedence relations only concern actions that share the same lifelines. Using the same notations, $e = 1.e_1 \cup 2.e_2$ and $o = 1.o_1 \cup 2.o_2 \cup \{(p_1, p_2)|p_1 \in 1.e_1, p_2 \in 2.e_2, \theta(i_{|p_1}) = \theta(i_{|p_2})\}$.

**Definition 4 (Orderings of a basic interaction).** We define the function $ord: \mathbb{B}(L, M) \to \mathcal{P}(\emptyset)$ as follows:

$$ord(\emptyset) = \{(\emptyset, \emptyset)\} \quad \text{and} \quad \forall act \in Act(L, M), ordPERT act = \{(\epsilon), \emptyset\}$$

For any $i_1$ and $i_2$ in $\mathbb{B}(L, M)$:

$$ord(alt(i_1, i_2)) = 1.ord(i_1) \cup 2.ord(i_2)$$

$$ord(par(i_1, i_2)) = \bigcup_{\substack{(e_1, o_1) \in ord(i_1) \\ (e_2, o_2) \in ord(i_2)}} \{(1.e_1 \cup 2.e_2, 1.o_1 \cup 2.o_2)\}$$

$$ord(strict(i_1, i_2)) = \bigcup_{\substack{(e_1, o_1) \in ord(i_1) \\ (e_2, o_2) \in ord(i_2)}} \left\{ (e, o) \middle| \begin{array}{l} e = (1.e_1 \cup 2.e_2), o = 1.o_1 \cup 2.o_2 \cup o' \\ o' = \{(p_1, p_2) \mid p_1 \in 1.e_1, p_2 \in 2.e_2\} \end{array} \right\}$$

$$ord(seq(i_1, i_2)) = \bigcup_{\substack{(e_1, o_1) \in ord(i_1) \\ (e_2, o_2) \in ord(i_2)}} \left\{ (e, o) \middle| \begin{array}{l} e = (1.e_1 \cup 2.e_2), o = 1.o_1 \cup 2.o_2 \cup o' \\ o' = \{(p_1, p_2) \mid \begin{array}{l} p_1 \in 1.e_1, p_2 \in 2.e_2 \\ \theta(i_{|p_1}) = \theta(i_{|p_2}) \end{array} \end{array} \right\}$$

A given ordering $(e, o)$ with $e = \{e_1, ..., e_n\}$ characterizes a set of behaviors that expresses every action whose position belongs to $e$ exactly once. Such a behavior is thus given under the form of an execution trace $i_{|e_{\alpha(1)}}, ..., i_{|e_{\alpha(n)}}$ where $\alpha$ is a permutation of $[1, n]$. Obviously, not all of those permutations are acceptable as they must not contradict the partial order specified by $o$. If we note $p_j = e_{\alpha(j)}$ for $j$ in $[1, n]$, we have $\forall j, k \in [1, n]^2 \ j > k \Rightarrow (p_j, p_k) \notin o$.

The semantics $\sigma(i)$ of an interaction $i$ then comes naturally as the union of all sets $sem(i, e, o)$ of execution traces of $i$ compatible with $(e, o) \in ord(i)$. When considering the example from Fig.2, we have $sem(i, \{11, 2\}, \{(11, 2)\}) = \{a!m_1.a!m_3\}$ and $sem(i, \{12, 2\}, \emptyset) = \{b?m_2.a!m_3, a!m_3.b?m_2\}$.
**Definition 5 (Denotational semantics for basic interactions).** For $i \in \mathbb{B}(L, M)$ and $(e, o) \in \text{ord}(i)$ with $n \in \mathbb{N}$ being the cardinal of $e$, we note:

$$ \text{sem}(i, e, o) = \{i_{|p_1} \dots i_{|p_n} | \forall (p_j, p_k) \in e^2, j > k \Rightarrow p_j \neq p_k \land (p_j, p_k) \notin o\} $$

$$ \sigma: \mathbb{B}(L, M) \to \mathcal{P}(\text{Act}(L, M)^*) \text{ is s. t. } \forall i \in \mathbb{B}(L, M), \sigma(i) = \bigcup_{(e,o) \in \text{ord}(i)} \text{sem}(i, e, o) $$

## 2.3 Extension of the language with loops

A loop is a repetition operator. Its content can be instantiated any finite number of times i.e multiple copies of it are inserted into the interaction. For UML-SD, the norm [23] states that "the loop construct represents a recursive application of the seq operator where the loop operand is sequenced after the result of earlier iterations". The UML-SD loop is hence associated with the seq operator. When instantiated, the loop content is ordered using seq this means for example that loop(a!m) becomes seq(a!m, loop(a!m)) then seq(a!m, seq(a!m, loop(a!m))) and so on. In line with this explanation, let's consider the 4 types of loops that can be characterized according to the operator ordering the instantiated content (seq, strict, par or alt). We can discard alt as instantiating loop(i) would lead to alt(i, loop(i)) meaning that the content can be read at most once and is therefore equivalent to opt(i) (i.e. alt(i, Ø)). We will here consider 3 operators denoted loopseq (the classical loop), loopstrict and looppar.

<figure><img src="image_4.png" /><figcaption>Fig. 3: Examples showcasing the pertinence of loopstrict and looppar</figcaption></figure>

In Fig.3-a-i, $i_{a|11} = a!m$ is the only immediately executable action and its execution leads to the interaction $i'_{a} = strict(b?m, i_{a})$ drawn on Fig.3-a-ii. Because of the strict operator, $i'_{a|211} = a!m$ is not immediately executable (preceded by $i'_{a|1} = b?m$). As a result $t_{a} = a!m.a!m.b?m.b?m$ is not an accepted trace for $i_{a}$. However, if there was a seq operator instead of the strict, $i'_{a|211}$ would be immediately executable and $t_{a}$ an accepted trace.

Similarly, in Fig.3-b-i, $i_{b|11} = a!m_{1}$ is the only immediately executable action and its execution leads to $i'_{b} = par(a!m_{2}, i_{b})$ drawn on Fig.3-b-ii. Because of the par operator, $i'_{b|211} = a!m_{1}$ is immediately executable. As a result $t_{b} = a!m_{1}.a!m_{1}.a!m_{2}.a!m_{2}$ is an accepted trace for $i_{b}$. However, if there was a seq
instead of the par, $i'_{b|211}$ would not be immediately executable and $t_b$ not an accepted trace.

Consequently, considering loop<sub>par</sub> and loop<sub>strict</sub> in addition to the classic loop<sub>seq</sub> improves expressiveness. In rough terms, loop<sub>par</sub> always allows new instantiations as each instance is executed in parallel w.r.t each others and the loop itself. loop<sub>strict</sub> on the contrary does not allow new instantiations as long as the previous instance has not been entirely executed. The behavior of loop<sub>seq</sub> is somewhat in the middle, instantiations being allowed depending on the current structure of actions preceding and within the loop.

In the following, we'll extend our IL to loops and adapt previous definitions (from $\mathbb{B}(L, M)$ to $\mathbb{I}(L, M)$). As in Def.6, any time we do so, we will only define the missing cases concerning loop terms.

**Definition 6 (Interactions).** The set $\mathbb{I}(L, M)$ of interactions over L and M is inductively defined as follows:

- $\emptyset \in \mathbb{I}(L, M)$ and $\mathrm{Act}(L, M) \subset \mathbb{I}(L, M)$,

- $\forall(i_1, i_2) \in \mathbb{I}(L, M)^2$ and $\forall f \in \{\mathrm{strict}, \mathrm{seq}, \mathrm{alt}, \mathrm{par}\}, f(i_1, i_2) \in \mathbb{I}(L, M)$,

- $\forall i \in \mathbb{I}(L, M)$ and $\forall f \in \{\mathrm{strict}, \mathrm{seq}, \mathrm{par}\}, \mathrm{loop}_f(i) \in \mathbb{I}(L, M)$.

The functions $\mathrm{ST}: \mathbb{I}(L, M) \to \mathcal{P}(\mathbb{I}(L, M))$, $\mathrm{pos}: \mathbb{I}(L, M) \to \mathcal{P}(\{1, 2\}^*)$ and $\mathrm{_\perp}: \mathbb{I}(L, M) \times \{1, 2\}^* \to \mathbb{I}(L, M)$ are defined by extending to loop terms the corresponding functions of Def.2:

For all $i$ in $\mathbb{I}(L, M)$ of the form $\mathrm{loop}_f(i')$ with $f \in \{\mathrm{strict}, \mathrm{seq}, \mathrm{par}\}$:

- $\mathrm{ST}(i) = \{i\} \cup \mathrm{ST}(i')$

- $\mathrm{pos}(i) = \{\epsilon\} \cup \mathrm{1.pos}(i')$,

- $i|_{\epsilon} = i$ and for $p = 1.p'$ in $\mathrm{pos}(i), i|_p = i'_{|p'}$.

In order to define the semantics of interactions, we use the notion of term replacement [7]: the notation $t[s]_p$ denotes the term $t$ where its subterm at position $p$ is replaced by the term $s$. For instance with $i = \mathrm{seq}(a!m, b?m)$, we have $i[c?m]_2 = \mathrm{seq}(a!m, c?m)$. This notation is convenient to represent terms obtained by loop unfolding. For example let us consider an interaction $i \in \mathbb{I}(L, M)$ with a loop<sub>seq</sub> at a position $p \in \mathrm{pos}(i)$, that is, such that $i|_p = \mathrm{loop}_{seq}(i|_{p.1})$. The interaction is then obtained from $i$ by unfolding once the loop at position $p$ is $i[\mathrm{seq}(i|_{p.1}, i|_p)]_p$. In Def.7, the set $\mathcal{Y}(i, n)$ of all n-unfoldings of an interaction $i$ (i.e. the set of all interactions resulting from $n$ instantiations of any loop from $i$) is defined recursively. On

Fig.4 loop unfolding is illustrated with $\mathcal{Y}(i, 0) = \{i\}$ and $\mathcal{Y}(i, 1) = \{i'\}$.

<figure><img src="image_5.png" /><figcaption>(a) $i = \mathrm{loop}_{seq}(i|_1)$
with $i|_1 = \mathrm{strict}(a!m, b?m)$</figcaption></figure>

<figure><img src="image_6.png" /><figcaption>(b) $i' = \mathrm{seq}(i|_1, i)$</figcaption></figure>

<caption>Fig. 4: Unfolding</caption>

**Definition 7 (n-unfoldings).** We define $\mathcal{Y}: \mathbb{I}(L, M) \times \mathbb{N} \to \mathcal{P}(\mathbb{I}(L, M))$ such that $\forall i \in \mathbb{I}(L, M) \mathcal{Y}(i, 0) = \{i\}$ and $\forall n \in \mathbb{N}^+$:

$$ \mathcal{Y}(i, n) = \bigcup_{p \in \mathrm{pos}(i) \text{ s.t. } i|_p = \mathrm{loop}_f(i|_{p.1})} \mathcal{Y}(i[f(i|_{p.1}, i|_p)]_p, n-1) $$
We define a function $F: \mathbb{I}(L, M) \to \mathbb{B}(L, M)$ that flattens interactions with loops i.e. that replaces all loop subterms with the empty interaction $\emptyset$. For instance, in Fig.4 we have $F(i) = \emptyset$ and $F(i') = seq(i_1, \emptyset)$. As $F(\mathbb{I}(L, M)) \subset \mathbb{B}(L, M)$, we can define an unfolding-based semantics<fnref n="7" /> for $i \in \mathbb{I}(L, M)$ by simply considering the union of semantics obtained from flattened unfoldings of $i$.

**Definition 8 (Denotational semantics for interactions).**

We define $\sigma_u : \mathbb{I}(L, M) \to \mathcal{P}(\mathcal{Act}(L, M)^*)$ such that for all $i$ in $\mathbb{I}(L, M)$:

$$ \sigma_u(i) = \bigcup_{n \in \mathbb{N}} \bigcup_{i' \in \mathcal{Y}(i,n)} \sigma(F(i')) $$

## 3 Operational Semantics

We aim to define algorithms that can determine whether or not a trace $t$ is accepted by an interaction $i$. This amounts to ascertaining whether or not $t \in \sigma_u(i)$. Naturally, being able to do so without having to compute $\sigma_u(i)$ is preferable. In the following we'll refer to this problem as 'trace analysis'.

As per Sec.2.3, asserting $t \in \sigma_u(i)$ equates to finding a combination of loop unfoldings $i^* \in \bigcup_{k=0}^{\infty} \mathcal{Y}(i, k)$ such that $t \in \sigma(F(i^*))$. Even if feasible, this would be time and space consuming<fnref n="8" />. As for non acceptation, it equates to proving that $\forall i^* \in \bigcup_{k=0}^{\infty} \mathcal{Y}(i, k)$ we have $t \notin \sigma(F(i^*))$. In this case, a termination in finite time would not even be guaranteed and would require defining some stopping criterion on the unfolding.

Consequently, we investigate another approach, in which traces are analyzed action by action. Here, instead of systematically unfolding loops, we do so on demand (when executing an *act* that is found within a loop). This approach is based on a different semantics ($\sigma_o$) whose description is the purpose of Sec.3.

$\sigma_o$ is presented in the style of operational semantics, i.e. consisting in: (1) identifying from the structure of $i$ which *act* can be immediately executed (coined 'frontier actions') and (2) deriving for each such *act* a new interaction $i'$ specifying all the possible continuations of *act* within the set of execution traces specified by $i$ (noted as $i \xrightarrow{act} i'$).

Intuitively, an action is in the frontier iff no structural operators (parent nodes) coerce it to be preceded by another action (sibling leaf). Accepted traces

<figure><img src="image_7.png" /><figcaption>Fig. 5: Operational Semantics</figcaption></figure>

<footnote n="7">⁷ coined $\sigma_u$, $u$ standing for 'unfolding-based'</footnote>

<footnote n="8">⁸ and would not be adaptable if one considers an extension to monitoring as new combinations $i^*$ may be needed every time a new action is observed</footnote>
are then built recursively through the successive consumption of actions. Let's consider a trace $t = act_1(...).act_n$ with $\forall k \in [1, n] i_{k-1} \xrightarrow{act_k} i_k$ and such that $i_0 = i$ (by extension we may note $i \xrightarrow{t} i_n$).

* If the last interaction $i_n$ can express the empty trace $\epsilon$ (i.e. $\epsilon \in \sigma_u(i_n)$) - which can be statically analysed - then $t$ is accepted by $i$ i.e. $t \in \sigma_o(i)$.

* In any case, for all frontier actions $act_{n+1}$ of $i_n$, we have $i_n \xrightarrow{act_{n+1}} i_{n+1}$, meaning that $t$ can be extended by $act_{n+1}$ and is a prefix of given trace(s) accepted by $i$.

To illustrate this, let's consider the example from Fig.5. The initial interaction is $i = seq(alt(a!m_1, b?m_2), a!m_3)$. There are 3 frontier actions that may play the role of act: $i_{|11} = a!m_1$, $i_{|12} = b?m_2$ and $i_{|2} = a!m_3$. The interactions remaining after the execution of $i_{|11}$ and $i_{|12}$ (resp. referred to as $i'_1$ and $i'_2$), which happen to be the same, are depicted below on the left, while the one remaining after the execution of $i_{|2}$ (noted $i'_3$) is depicted on the right. The cases leading to $i'_1$ and $i'_2$ are self-evident. As for the one leading to $i'_3$, the execution of $a!m_3$ is contingent to the choice of the branch 12 of the alt hence the elimination of branch 11 in the remaining interaction. Indeed, if branch 11 were to be chosen, the execution of $a!m_3$ would not be possible as $a!m_1$ should have been executed before. This illustrates that $a!m_3$ is a frontier action up to the choice of the right branch of the alt operator. Let us remark that $b?m_2$ may indeed happen after $a!m_3$ as those two actions occur on different lifelines and the top seq operator structuring them does not constrain their order of execution. Finally, we conclude by defining the operational semantics as $\sigma_o(i) = a!m_1 \cdot \sigma_o(i'_1) \cup b?m_2 \cdot \sigma_o(i'_2) \cup a!m_3 \cdot \sigma_o(i'_3)$.

## 3.1 Frontier actions

In this section we explain how to identify frontier actions. Our notion of frontier differs slightly from that of [4], where it refers to the set of positions $p$ such that $\forall j \in \{1, 2\}^*$, $p.j \notin pos(i)$ (i.e. positions of leaf nodes). Indeed, our frontiers contain only leaves that are immediately executable actions.

Any ordering as defined in Def.4 provides a partial order relation for the set of (positions of) actions of a basic interaction. A frontier action act on position $p$ is then simply a minimal element given such a relation $(e, o)$, i.e. s.t. $\forall p' \in e$ we have $(p', p) \notin o$ i.e. act does not have to be preceded by any other action. The frontier of an interaction $i$ is then defined as the union of such $p$, considering all the orderings from ord($i$). As Def.4 did not include loop operators, we extend it in the following definition, in which the empty ordering $(\emptyset, \emptyset)$ corresponds to the case where the loop has not unfolded. According to this, the frontier of $i$ from Fig.5 is then $front(i) = \{11, 12, 2\}$.

**Definition 9 (Ordering).** We define ord : $\mathbb{I}(L, M) \to \mathcal{P}(\emptyset)$ as an extension to $\mathbb{I}(L, M)$ of its counterpart from Def.4. For all $f$ in $\{\text{strict}, \text{seq}, \text{par}\}$:

$$ \forall i \in \mathbb{I}(L, M), \mathrm{ord}(\mathrm{loop}_f(i)) = 1.\mathrm{ord}(i) \cup \{(\emptyset, \emptyset)\} $$

**Definition 10 (Frontier).** $front : \mathbb{I}(L, M) \to \mathcal{P}(\{1, 2\}^*)$ is the function s.t.:

$$ \forall i \in \mathbb{I}(L, M), front(i) = \bigcup_{(e,o) \in \mathrm{ord}(i)} \{p \in e \mid \forall p' \in e, (p', p) \notin o\} $$
## 3.2 Pruning

The design of the rules $i \xrightarrow{act} i'$ hinted at earlier is made operational thanks to 2 mechanisms: pruning and execution. Given an action *act* ∈ *front*(*i*), branches preventing its execution are detected and eliminated with pruning. However, this is not done on the whole interaction *i* but rather on specific neighboring (w.r.t. *act*) subinteractions. Execution orchestrates the calls to pruning, eliminates *act* and constructs the remaining interaction *i*.'

<figure><img src="image_8.png" /><figcaption>Fig. 6: Example showcasing pruning</figcaption></figure>

We first define the pruning mechanism which consists in removing from an interaction all the actions which occur on a given lifeline. For instance, on Fig. 6-b, let us consider the interactions $i_1 = i|_1 = loop_{seq}(strict(a!m_1, b?m_1))$ and $i_2 = i|_{21} = loop_{seq}(alt(a!m_2, b?m_3))$ highlighted in green. We want to remove actions occurring on the lifeline *a* (so as to allow the execution of $i|_{22} = a!m_4$). We find that $i_1|_{11} = a!m_1$ (resp. $i_2|_{11} = a!m_2$) needs to be removed from $i_1$ (resp. $i_2$). If we do not want to get an interaction which is inconsistent or outwardly contradicts the original semantics, we can only prune subinteractions at positions where branching choices are made i.e. in *alt* and *loop* nodes. Indeed, by definition, eliminating a subinteraction at one such node would lead to a semantics that is included in the original.

In $i_2$, eliminating $i_2|_{11}$ is easily done given that its parent node is an *alt* and that its brother node does not need to be eliminated. Indeed, it suffices to operate the replacement $i_2[i_2|_{12}]_1$ i.e. replacing the *alt* node with its right child $b?m_3$.

In $i_1$, eliminating $i_1|_{11}$ is more delicate: its parent node is a *strict* and as such, behaviors from its left and right children must both happen (there is no branching choice). Thus, if we want to eliminate $i_1|_{11}$ we must also eliminate the whole $i_1|_1$. The problem is hence forwarded upwards in the syntax. The parent $i_1|_\epsilon$ is a loop operator, which characterizes a branching choice. We can eliminate the problematic branch by choosing not to instantiate the loop i.e. via the replacement $i_1[\emptyset]_\epsilon$.
The pruning mechanism is given in Def. 11 as the recursive `prune` function, which takes as arguments an interaction `i` and a lifeline `l`. `prune` eliminates from `i` branching choices hosting actions that occur on `l`.

In a first descending phase, `prune` goes down the syntax of `i` through recursive calls (from root to leaves). When reaching a leaf, `prune` returns an interaction `i'` and a boolean `b`. `b = ⊤` signifies that the current branch needs to be eliminated (pruned) while `i'` is the interaction that will be used to reconstruct `i` in the ascending phase (only used if `b = ⊥`). Leaves are either actions or empty interactions. For an action `act`, if $\theta(\mathit{act}) = l$, the current branch must be pruned so $\mathit{prune}(\mathit{act}, l) = (\emptyset, ⊤)$: the value of the returned interaction `i'` has no importance here because a parent will be pruned anyway. If $\theta(\mathit{act}) \neq l$ we have $\mathit{prune}(\mathit{act}, l) = (\mathit{act}, ⊥)$ because there is nothing to prune here. Similarly, we have $\mathit{prune}(\emptyset, l) = (\emptyset, ⊥)$.

In the second, ascending phase, the pruned interaction is reconstructed according to the values of `i'` and `b` returned from child branches. If at any point `b = ⊤`, this value is forwarded upwards until an expendable branching choice is reached.

`prune(i, l)` is recursively called on the child nodes of `i`. Depending on the operator in `i`, the return values of `prune(i|1, l) = (i'_1, b_1)` (and also `prune(i|2, l) = (i'_2, b_2)` for binary operators) will be used differently to determine `i'` and `b`.

For the operators $f \in \{\mathit{strict}, \mathit{seq}, \mathit{par}\}$, if any one child must be pruned ($b_1 \lor b_2$) then the whole branch must also be pruned and otherwise a reconstructed $f(i'_1, i'_2)$ is returned. For the exclusive alternative `alt`, if no branch needs pruning, `alt(i'_1, i'_2)` is returned; if any single branch needs pruning, `prune` returns the one that does not need to be pruned and if both branches need pruning, then the whole interaction is pruned. For the repetition operators, if the loop content needs pruning then the choice of 'never taking the loop' is made meaning that $\emptyset$ is returned with $b = ⊥$, signifying a successful pruning. If there is no needed pruning, it simply returns the loop with an already pruned loop content $\mathit{loop}_f(i'_1)$.

**Definition 11 (Pruning).** `prune`: $\mathbb{I}(L, M) \times L \rightarrow \mathbb{I}(L, M) \times \mathit{bool}$ is the function such that for all $i \in \mathbb{I}(L, M)$ and $l \in L$:

- $\mathit{prune}(\emptyset, l) = (\emptyset, \bot)$

- for $\mathit{act} \in \mathit{Act}(L, M)$: if $\theta(\mathit{act}) = l$ then $\mathit{prune}(\mathit{act}, l) = (\emptyset, \top)$ (else $(\mathit{act}, \bot)$)

- if $i = f(i_1, i_2)$ with $f \in \{\mathit{strict}, \mathit{seq}, \mathit{par}\}$, given $\mathit{prune}(i_1, l) = (i'_1, b_1)$ and $\mathit{prune}(i_2, l) = (i'_2, b_2)$:

if $b_1 \lor b_2$ then $\mathit{prune}(i, l) = (\emptyset, \top)$ (else $(f(i'_1, i'_2), \bot)$)

- if $i = \mathit{alt}(i_1, i_2)$, given $\mathit{prune}(i_1, l) = (i'_1, b_1)$ and $\mathit{prune}(i_2, l) = (i'_2, b_2)$:

* if $b_1 \land b_2$ then $\mathit{prune}(i, l) = (\emptyset, \top)$

* if $b_1 \land \neg b_2$ then $\mathit{prune}(i, l) = (i'_2, \bot)$

* if $\neg b_1 \land b_2$ then $\mathit{prune}(i, l) = (i'_1, \bot)$

* if $\neg b_1 \land \neg b_2$ then $\mathit{prune}(i, l) = (\mathit{alt}(i'_1, i'_2), \bot)$

- if $i = \mathit{loop}_f(i_1)$ with $f \in \{\mathit{strict}, \mathit{seq}, \mathit{par}\}$, given $\mathit{prune}(i_1, l) = (i'_1, b_1)$:

if $b_1$ then $\mathit{prune}(i, l) = (\emptyset, \top)$ (else $(\mathit{loop}_f(i'_1), \bot)$)
### 3.3 Execute function and operational semantics

Let us consider the example *i* from Fig.6. We wish to execute the frontier action $i_{|22} = alm_4$ (highlighted in red). To allow this execution we need at first to remove the actions occurring on the same lifeline (i.e. on *a*) from the neighbors highlighted in green. To do so, we use the *prune* function from Def.11. More generally, the nature of our syntax is such that, for the execution of a frontier action at position *p*, we only need to prune subinteractions at positions $p_0$.1 s.t. $\exists p' \in \{1, 2\}^*$ s.t. $p = p_0$.2.p' and s.t. $i_{|p_0} = seq(i_{|p_0.1}, i_{|p_0.2})$. Those are exactly the left cousins of $i_{|p}$ that are scheduled sequentially (i.e. with *seq*) w.r.t. $i_{|p}$.

We now define the execution function $\chi$ (Def.12), which takes as arguments an interaction *i* and a frontier position *p* and returns the remaining interaction $i'$. As explained earlier, $\chi$ orchestrates the use of *prune*. In the example from Fig.6 this first cleaning feature would result in the transformation of *i* from the diagram on Fig.6-a to the one on Fig.6-c. The only thing left to do is then to remove the executed action s.t. the result is the interaction from Fig.6-d.

$\chi$ is defined inductively on both the structure of the interaction *i* and the position $p = d_1...d_n \in \{1, 2\}^n$. The execution of $\chi(i, p)$ traverses recursively the syntactic structure of *i* guided by the path defined by the position *p*, that is, from $\chi(i|_\epsilon, d_1...d_n)$ (root node), ..., up to $\chi(i|_p, \epsilon)$ (target action leaf to execute). Here, $\chi(i|_p, \epsilon) = \emptyset$ constitutes the stopping criterion and $i'$ is then constructed when the algorithm goes back up through the syntactic structure of *i*. Assigning $\emptyset$ to $\chi(i|_p, \epsilon)$ ensures that the action $i|_p$ is removed in the construction of $i'$.

When a *par* node is encountered during the upward traversal, i.e. for $j \in [1, n]$, $i_{|d_1...d_j} = par(i_{|d_1...d_{j-1}}, i_{|d_1...d_{j-2}})$ then $\chi(i_{|d_1...d_j}, d_{j+1}...d_n)$ is simply:

$par(\chi(i_{|d_1...d_{j-1}}, d_{j+2}...d_n), i_{|d_1...d_{j-2}})$ if $d_{j+1} = 1$ or,

$par(i_{|d_1...d_{j-1}}, \chi(i_{|d_1...d_{j-2}}, d_{j+2}...d_n))$ if $d_{j+1} = 2$.

Indeed, as *par* specifies parallel executions, there is no need for pruning.

When an *alt* node is reached, using the same notations, we would have:

$$\chi(i_{|d_1...d_j}, d_{j+1}...d_n) = \chi(i_{|d_1...d_{j+1}}, d_{j+2}...d_n).$$

Indeed, we can 'skip' the *alt* node itself and replace it directly with the interaction resulting from the execution of the chosen branch.

When a *loop* is reached, i.e. $i_{|d_1...d_j} = loop_f(i_{|d_1...d_{j-1}})$ (with a mandatory $d_{j+1} = 1$), we have:

$$\chi(i_{|d_1...d_j}, d_{j+1}...d_n) = f(\chi(i_{|d_1...d_{j+1}}, d_{j+2}...d_n), i_{|d_1...d_j}).$$

Indeed, the execution is done on a copy of the loop content that precedes (with *f* operator) the loop $i_{|d_1...d_j}$ itself, that is, on an unfolding of the loop.

For the sequential operators, pruning needs to be considered only if the executing action is situated on the right branch of the *seq* or *strict* node (if the action is on the left branch, we have the same transformation as in the *par* case). Given $i_{|d_1...d_j} = seq(i_{|d_1...d_{j-1}}, i_{|d_1...d_{j-2}})$ and $d_{j+1} = 2$, when constructing $\chi(i_{|d_1...d_j}, d_{j+1}...d_n)$ we must prune in $i_{|d_1...d_{j-1}}$ all the actions that could interfere with $i_{|p}$ i.e. those taking place on $\theta(i_{|p})$. As such, given $(i'_1, b_1) = prune(i_{|d_1...d_{j-1}}, \theta(i_{|p}))$, we'll replace the left branch of the *seq* with $i'_1$ and reconstruct:

$$\chi(i_{|d_1...d_j}, d_{j+1}...d_n) = seq(i'_1, \chi(i_{|d_1...d_{j+1}}, d_{j+2}...d_n)).$$
Given that the strict operator won't allow any action from the left branch to occur after an action on the right has occurred, we can simply prune the whole left branch i.e. given $i_{|d_1...d_j} = strict(i_{|d_1...d_j.1}, i_{|d_1...d_j.2})$ and $d_{j+1} = 2$:

$$ \chi(i_{|d_1...d_j}, d_{j+1}...d_n) = \chi(i_{|d_1...d_{j+1}}, d_{j+2}...d_n). $$

**Definition 12 (Execution).** The function $\chi: \mathbb{I}(L, M) \times \{1, 2\}^* \to \mathbb{I}(L, M)$ is defined for couples $(i, p)$ with $i \in \mathbb{I}(L, M)$ and $p \in \text{front}(i)$ as follows:

- if $p = \epsilon$ then $\chi(i, p) = \emptyset$

- if $p = 1.p_1$ then

* if $i = f(i_1, i_2)$ with $f \in \{\text{strict}, \text{seq}, \text{par}\}$ then $\chi(i, p) = f(\chi(i_1, p_1), i_2)$

* if $i = \text{alt}(i_1, i_2)$ then $\chi(i, p) = \chi(i_1, p_1)$

* if $i = \text{loop}_f(i_1)$ with $f \in \{\text{strict}, \text{seq}, \text{par}\}$ then $\chi(i, p) = f(\chi(i_1, p_1), i)$

- if $p = 2.p_2$ then

* if $i = \text{seq}(i_1, i_2)$ then $\chi(i, p) = \text{seq}(i'_1, \chi(i_2, p_2))$ where $\text{prune}(i_1, \theta(i_p)) = (i'_1, b)$

* if $i = \text{strict}(i_1, i_2)$ then $\chi(i, p) = \chi(i_2, p_2)$

* if $i = \text{par}(i_1, i_2)$ then $\chi(i, p) = \text{par}(i_1, \chi(i_2, p_2))$

* if $i = \text{alt}(i_1, i_2)$ then $\chi(i, p) = \chi(i_2, p_2)$

In Def.13 below, we now define the operational semantics. Note that interactions that can express the empty trace $\epsilon$ are identified with the predicate $\text{exp}_\epsilon$. This semantics expresses rules of the form $i \stackrel{i|p}{\to} \chi(i, p)$ where $p \in \text{front}(i)$.

**Definition 13 (Operational semantics for interactions).**

We define $\sigma_o: \mathbb{I}(L, M) \to \mathcal{P}(\text{Act}(L, M)^*)$ as:

$$ \sigma_o(i) = \text{empty}(i) \cup \bigcup_{p \in \text{front}(i)} i_{|p} \cdot \sigma_o(\chi(i, p)) $$

with $\text{empty}(i) = \{\epsilon\}$ ($\text{resp.}\emptyset$) if $\text{exp}_\epsilon(i) = \top$ ($\text{resp.}\perp$)

where $\text{exp}_\epsilon: \mathbb{I}(L, M) \to \text{bool}$ is defined as:

- $\text{exp}_\epsilon(\emptyset) = \top$

- $\text{exp}_\epsilon(l\Delta m) = \perp$

- $\text{exp}_\epsilon(f(i_1, i_2)) = \text{exp}_\epsilon(i_1) \wedge \text{exp}_\epsilon(i_2)$ for $f \in \{\text{strict}, \text{seq}, \text{par}\}$

- $\text{exp}_\epsilon(\text{alt}(i_1, i_2)) = \text{exp}_\epsilon(i_1) \vee \text{exp}_\epsilon(i_2)$

- $\text{exp}_\epsilon(\text{loop}_f(i_1)) = \top$ for $f \in \{\text{strict}, \text{seq}, \text{par}\}$

# 4 Back-to-back comparison of both semantics

**Dataset.** The recursive definition of interactions as syntactic terms allows to characterize them by their depth. Interactions of depth 1 include the empty interaction $\emptyset$ and all actions from $\text{Act}(L, M)$. Depending on the cardinals $n_l = \text{Card}(L)$ and $n_m = \text{Card}(M)$, those interactions can all be enumerated and computed. Given a signature, interactions of depth 2 can be deduced from those of depth 1 and exhaustively computed via the application of the binary and unary operators (e.g. $\text{seq}(\emptyset, a!m)$). Likewise, interactions of depth 3 can be computed from those of depths 1 and 2 and so on. To illustrate this, Fig.7 presents for each couple $(n_l, n_m)$ the numbers of interactions of depths 1, 2 and 3 in each cell. For instance, we have 3 interactions of depth 1 for $n_l = n_m = 1$.
**Experiments.** We implemented both semantics ($\sigma_u$ from Def.8 and $\sigma_o$ from Def.13) and compared the set of traces $\sigma_u(i)$ and $\sigma_o(i)$ they generate (with a stopping criterion on the maximum number of loop unfolding - 4 in our experiments) on a significant set of interactions of depth 3 with $n_l = n_m = 3$. For all of the 234175 selected interactions $i$ from our dataset, the tests systematically concluded on the equality $\sigma_u(i) = \sigma_o(i)$. Although not a proof, our successful back-to-back comparison comforts our confidence in both semantics, all the more so because of the exhaustivity of the subject data set up to maximum numbers of lifelines, messages types, interaction depth (up to 3), number of loop unfolding (up to 4), allowing covering all 2 by 2 combinations of operators.

Fig. 7: Numbers of interactions per $n_l$, $n_m$ and $d$

<table><thead><tr><th>n<sub>m</sub> n<sub>l</sub></th><th>1</th><th>2</th><th>3</th></tr></thead><tbody><tr><td rowspan="3">1</td><td>3</td><td>5</td><td>7</td></tr><tr><td>45</td><td>115</td><td>217</td></tr><tr><td>9315</td><td>57845</td><td>201159</td></tr><tr><td rowspan="3">2</td><td>5</td><td>9</td><td>13</td></tr><tr><td>115</td><td>351</td><td>715</td></tr><tr><td>57845</td><td>519129</td><td>2121405</td></tr><tr><td rowspan="3">3</td><td>7</td><td>13</td><td>19</td></tr><tr><td>217</td><td>715</td><td>1501</td></tr><tr><td>201159</td><td>2121405</td><td>9244659</td></tr></tbody></table>

## 5 Trace analysis

The definition of the execution function $\chi$ (Def.12) that comes with the operational nature of the $\sigma_o$ semantics (Def.13) allows us to solve the 'trace analysis' problem hinted at earlier. Indeed, analysing a trace $t = act_1...act_n$ w.r.t. an interaction $i_0$ equates to verifying whether or not there exists transformations $i_0 \xrightarrow{act_1} \chi(i_0, p_1) = i_1, ..., i_{n-1} \xrightarrow{act_n} \chi(i_{n-1}, p_n) = i_n$ s.t. $i_n$ accepts the empty trace.

We define an $\omega$ function (Def.14) which takes as arguments an interaction $i$ and a trace $t$ and checks whether or not $t$ is a trace of $i$. Additional traceability information is provided using four distinct verdicts:

* Covered is returned when $t$ is a trace of $i$ i.e. $t \in \sigma_o(i)$;

* TooShort is returned when $t \notin \sigma_o(i)$ is a strict prefix of a trace of $i$ i.e. $\exists t' \in Act(L, M)^*$ s.t. $t.t' \in \sigma_o(i)$;

* TooLong is returned when neither Covered nor TooShort can be, and given $t = act_1...act_n \exists k < n$ s.t. $act_1...act_k \in \sigma_o(i)$ i.e. $t$ extends a trace of $i$;

* Out is returned when none of the others can be.

We define the enumerated type Verdict and provide it with a total order Out $\prec$ TooLong $\prec$ TooShort $\prec$ Covered.

<figure><img src="image_9.png" /><figcaption>Fig. 8: Application of $\omega$</figcaption></figure>

* If $t$ is empty then: either $i$ accepts the empty trace in its semantics and in this case $\omega(i, t)$ returns Covered, or it returns TooShort.

* If $t$ is of the form $act.t'$ (i.e. not empty and starts with $act$) then, for all matching actions $i|_p$ in the frontier of $i$, recursive calls are performed on $\omega(\chi(i, p), t')$ and $\omega(i, t)$ returns the strongest ($\max_{\prec}$ function) verdict among those and either TooLong if $i$ expresses the empty trace $\epsilon$ or Out if not.
The linear regression shows curves with a great variability (some traces need 4 seconds while others only 0.06). In this precise model, it is explained by the presence of *par* (via *loop*<sub>par</sub>) operators and by the fact that messages are not uniquely identified. For instance analyzing *t* = *a!*·*b?m* on *i* = *par*(*a!*·*strict*(*a!*·*b?m*)) would give rise to 2 branches: *i'* = *strict*(*a!*·*b?m*) (resp. *i'* = *par*(*a!*·*b?m*)) with *t'* = *b?m* which ends with *Out* (resp. *Covered*) because *m* is not uniquely identified. This number of branches can quickly explode when *par* operators are stacked which happens when the trace describes an execution where many

loop content instances overlap. An applicable solution is to treat message data arguments, given that communication protocols provide unique ids e.g. *m*(*id1*) ≠ *m*(*id2*). In Fig.10-b, on the plot below, we magnified on traces 9, 34 & 61 which have a very short analysis time. We can surmise here that minimal (perhaps no) loop overlap occurred as the derivatives are almost constants (especially for trace 61). In conclusion, performance highly depends on the model and input trace, but treating data which specifies unique ids for messages would generalize the best case scenario. In this case, the algorithm could be applied to monitoring within the limits of an input frequency that is inferior to the time required to analyze a trace of length 1.

Fig. 10: Performances

<figure><img src="image_10.png" /><figcaption></figcaption></figure>

# 6 Related work

For classical IL such as UML-SD or HMSC, many authors have proposed their own takes on formal semantics (see the survey [21] for UML-SD).

**Denotational Semantics.** Most existing semantics based on term interpretations are given in a denotational style [27,14,3,17] and do not follow-up with algorithmic tools. In [27], the authors propose a denotational semantics similar to ours (Def.5) as far as the *strict*, *alt* and *par* operators are concerned. [14] proposes a semantics that is a detailed version of the one from [27]. In [17] there is a distinction (*snd*(*s*, *r*, *m*)|*snd*(*s*, *m*)|*rcv*(*s*, *r*, *m*)|*rcv*(*r*, *m*)) between basic actions whether or not the intended receiver or original sender is the environment. Apart from that, and the absence of *loops*, the denotational semantics proposed by [17] is similar to ours. In [3], an institutional approach, likened to that of [17] is proposed. However it includes *loops* and deals with modalities associated to
the *neg* and *assert* operators [23] by separating the semantics in sets of accepted and refused traces. This issue of modality is also raised in [21] and [13] but it is out of the scope of this paper.

**Translations based approaches.** Most other approaches rely on translations that map concepts of the given IL into a target formal framework, most often based on automata [11,2,28,19] or Petri nets [8,5,10]. Albeit those translations allow reusing advantageously the target framework’s tools, relying on them to capture semantics leads to reasoning on foreign concepts. In [11], UML-SDs are translated into timed automata, which are then verified with the UPPAAL tool [18]. The translation mechanisms only concern models with synchronous communications. An observer automaton has to be designed so as to intercept communications between automata, make them observable, and enter an error state if other events are observed. In [2], each lifeline is translated into a timed input output symbolic transition system (TIOSTS) and message passing relies on some synchronous product. In order to cope with asynchronism, FIFO based communication schema have been introduced to ensure the consistency of executions on different lifelines. Also, dedicated variables have to be introduced to keep track of branching choices specified by *alt* or *loop* operators. In [28], a symbolic automaton is built from UML-SD specifications in the goal of analyzing traces by means of valid, invalid or inconclusive verdicts. [19] focuses on how to test Message Sequence Charts when the system is only partially observed. A translation into a network of asynchronous concurrent automata allows to define semantics through a product automaton as in [2]. In [8], UML-SD specifications are translated into multivalued nets (M-nets). The translation is compositional, entry and exit places of the M-nets corresponding to subinteractions being connected differently according to the parent combined fragment. However this process is complicated by the tracking of actions that are completely unordered w.r.t. one another. [8] also treats data in the form of variables, message parameters and guards. In [5], the authors propose an approach to automatically translate UML-SDs designed with the Papyrus tool [12] to Coloured Petri Nets (CPNs) in a format compatible with CPNTools [16]. CPNs come with an execution semantics that is particularly adapted for the description and analysis of distributed and concurrent systems. In [5], the translation revolves around a list of 11 rules with different priorities and which are applied to translate different concepts (lifelines, message occurrences, combined fragments, etc.) while iterating sequentially through the UML-SD’s elements. In [10] a set of UML-SDs are translated into Extended Petri Nets. Input execution traces can then be checked against the EPNs.

**Operational approach.** The literature contains few attempts at defining operational semantics for ILs. In [26], the authors build formal expressions over a process algebra signature. Starting from axioms such as $\epsilon \downarrow$ (the empty process $\epsilon$ terminates) and $a \xrightarrow{a} \epsilon$ ($a$ being an atomic action), an expression describing a MSC is build using rules such as $(x \xrightarrow{a} x') \land (y \not\xrightarrow{a} y) \Rightarrow (x \mp y \xrightarrow{a} x')$. Such an expression is then associated with a transition graph. The contribution in [26] does not however deal with *loop* operator and it is quite different from ours as
the proposed transformations operate on process-algebraic expressions and not
on syntactic terms. In contrast, the semantics proposed in [20] relies on syn-
tactic term transformations. Still, it also requires a communication medium as
it is defined as the output of a combination of two transitions systems: an ex-
ecution system which keeps track of communications, and a projection system
which selects the next action to execute and provide the resulting interaction.
As explained in [9], communication models keep track of emitted messages and
messages pending receptions. They can for instance take the form of a set of
dedicated buffers (e.g. FIFO). Our approach has the advantage of making such
communication models implicit.

**Discussions.** Despite interaction languages specifying no synchronisation mech-
anisms between lifelines, several approaches that aim to implement tools, impose
synchronisation points when entering and exiting combined operators and at de-
cision points (alt, opt, loop) [28,2,8,21] (although more recent works such as
[10,20] do not). Although translation-based approaches have the benefit of al-
lowing the use of the many existing analysis tools (UPPAAL [18], DIVERSITY
[15], CPNTools [16] etc.) we postulate that direct operational approaches such
as ours facilitate features such as animation and debugging, becoming for the
most part free-of-charge by-products of the analysis process.

7 Conclusion

In this paper we proposed an operational semantics for ILs, aimed at trace valid-
ity analysis. This semantic is built upon a formal syntax for interaction terms and
validated back-to-back w.r.t. a reference denotational semantics. Our semantics
is built on partial order relations induced on messages by the syntax. Those re-
lations allow the identification of immediately executable actions. Pruning tech-
niques then ensure a consistent semantics based on successive transformations of
the form i $^{act}$→ i'. On this principle, we have defined and implemented algorithms
to compute semantics and to analyze the validity of traces. Experiments were
successfully conducted in order to evaluate the correctness of each.

We intend to enrich our formalism: (1) by expanding trace analysis to a
distributed context, where a set of traces (multi-trace) may be analyzed concur-
rently on a subset of observed lifelines; (2) by investigating whether or not our
algorithmic treatments are fast enough to deal with traces on-the-fly so as to
adapt them to monitoring. (3) by extending our IL to include modality oper-
ators such as *assert* or *negate*. (4) by allowing the use of message arguments,
variables, clocks and constraints within models.

Additionally, it would be interesting to perform a comparison with translation-
based approaches. This may consist in a comparison of formal semantics and/or
in benchmarking implementations according to a certain performance metric.
References

1. Alur, R., Yannakakis, M.: Model checking of message sequence charts. In: CONCUR '99: Concurrency Theory. Lecture Notes in Computer Science, vol. 1664, pp. 114–129. Springer (1999)

2. Bannour, B., Gaston, C., Servat, D.: Eliciting unitary constraints from timed sequence diagram with symbolic techniques: Application to testing. In: 2011 18th Asia-Pacific Software Engineering Conference. pp. 219–226 (2011)

3. Cengarle, M., Knapp, A.: An institution for uml 2.0 interactions (01 2008)

4. Comon, H., Dauchet, M., Gilleron, R., Löding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (10 2007)

5. Custódio Soares, J.a.A., Lima, B., Pascoal Faria, J.a.: Automatic model transformation from uml sequence diagrams to coloured petri nets. In: Proceedings of the 6th International Conference on Model-Driven Engineering and Software Development. p. 668–679. MODELSWARD 2018, SCITEPRESS - Science and Technology Publications, Lda, Setubal, PRT (2018). https://doi.org/10.5220/0006731806680679

6. Damm, W., Harel, D.: Lscs: Breathing life into message sequence charts. Formal Methods in System Design **19**(1), 45–80 (2001)

7. Dershowitz, N., Jouannaud, J.P.: Handbook of theoretical computer science (vol. b). chap. Rewrite Systems, pp. 243–320. MIT Press, Cambridge, MA, USA (1990)

8. Eichner, C., Fleischhack, H., Meyer, R., Schrimpf, U., Stehno, C.: Compositional semantics for uml 2.0 sequence diagrams using petri nets. In: Prinz, A., Reed, R., Reed, J. (eds.) SDL 2005: Model Driven. pp. 133–148. Springer Berlin Heidelberg, Berlin, Heidelberg (2005)

9. Engels, A., Mauw, S., Reniers, M.: A hierarchy of communication models for message sequence charts. Science of Computer Programming **44**(3), 253 – 292 (2002). https://doi.org/10.1016/S0167-6423(02)00022-9

10. Faria, J.P., Paiva, A.C.R.: A toolset for conformance testing against uml sequence diagrams based on event-driven colored petri nets. International Journal on Software Tools for Technology Transfer **18**(3), 285–304 (2016)

11. Firley, T., Huhn, M., Diethers, K., Gehrke, T., Goltz, U.: Timed sequence diagrams and tool-based analysis - A case study. In: UML'99: The Unified Modeling Language - Beyond the Standard. Lecture Notes in Computer Science, vol. 1723, pp. 645–660. Springer (1999)

12. Gérard, S., Dumoulin, C., Tessier, P., Selic, B.: Papyrus: A UML2 Tool for Domain-Specific Language Modeling, pp. 361–368. Springer Berlin Heidelberg, Berlin, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16277-0_19

13. Harel, D., Maoz, S.: Assert and negate revisited: Modal semantics for UML sequence diagrams. Software and Systems Modeling **7**(2), 237–252 (2008)

14. Haugen, O., Husa, K.E., Runde, R.K., Stølen, K.: STAIRS towards formal design with sequence diagrams. Software and Systems Modeling **4**(4), 355–367 (2005)

15. Hussein, M., Nouacer, R., Radermacher, A., Puccetti, A., Gaston, C., Rapin, N.: An end-to-end framework for safe software development. Microprocessors and Microsystems **62**, 41 – 49 (2018). https://doi.org/10.1016/j.micpro.2018.07.004

16. Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri Nets and CPN Tools for modelling and validation of concurrent systems. International Journal on Software Tools for Technology Transfer **9**(3), 213–254 (Jun 2007). https://doi.org/10.1007/s10009-007-0038-x
17. Knapp, A., Mossakowski, T.: UML Interactions Meet State Machines - An Institutional Approach. In: 7th Conf. on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), vol. 72, pp. 15:1–15:15. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (2017)

18. Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. International Journal on Software Tools for Technology Transfer **1**(1), 134–152 (Dec 1997).
https://doi.org/10.1007/s100090050010

19. Longuet, D.: Global and local testing from message sequence charts. In: Proceedings of the ACM Symposium on Applied Computing, SAC 2012. pp. 1332–1338. ACM (2012)

20. Lund, M.S., Stølen, K.: A fully general operational semantics for uml 2.0 sequence diagrams with potential and mandatory choice. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006: Formal Methods. pp. 380–395. Springer Berlin Heidelberg, Berlin, Heidelberg (2006)

21. Micskei, Z., Waeselynck, H.: The many meanings of uml 2 sequence diagrams: a survey. Software & Systems Modeling **10**(4), 489–514 (2011)

22. OASIS: Mqd version 3.1.1 (12 2015)

23. OMG: Unified Modeling Language v2.5.1 (12 2017)

24. Plotkin, G.D.: An operational semantics for CSP. In: Formal Description of Programming Concepts: Proceedings of the IFIP Working Conference on Formal Description of Programming Concepts - II. pp. 199–226. North-Holland (1983)

25. S., M., M. A., R.: High-level message sequence charts. In: SDL '97 Time for Testing, SDL, MSC and Trends - 8th International SDL Forum, Proceedings. pp. 291–306. Elsevier (1997)

26. S., M., M. A., R.: Operational semantics for msc. Computer Networks **31**(17), 1785–1799 (1999)

27. Storrle, H.: Semantics of interactions in uml 2.0. In: IEEE Symposium on Human Centric Computing Languages and Environments, 2003. Proceedings. 2003. pp. 129–136 (Oct 2003).
https://doi.org/10.1109/HCC.2003.1260216

28. Waeselynck, H., Micskei, Z., Rivière, N., Hamvas, Á., Nitu, I.: Termos: A formal language for scenarios in mobile computing systems. In: Sénac, P., Ott, M., Seneviratne, A. (eds.) Mobile and Ubiquitous Systems: Computing, Networking, and Services. pp. 285–296. Springer Berlin Heidelberg, Berlin, Heidelberg (2012)

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

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