key: cord-0048639-7blh7dp6
authors: Mahe, Erwan; Gaston, Christophe; Gall, Pascale Le
title: Revisiting Semantics of Interactions for Trace Validity Analysis
date: 2020-03-13
journal: Fundamental Approaches to Software Engineering
DOI: 10.1007/978-3-030-45234-6_24
sha: 3d0766641883a3778b54c4af699b3a65f686dc05
doc_id: 48639
cord_uid: 7blh7dp6

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.

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 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. When ILs are fitted with formal semantics, requirements can be processed using formal techniques, such as modelchecking [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 semantics, 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 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

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∆m|l ∈ L, ∆ ∈ {!, ?}, m ∈ 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∆m, Θ(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). The empty interaction ∅ 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 = 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 , 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 ∈ pos(i) (cf. example in Fig.2 ). 3 Note that we omit depicting seq on diagrams as is classically done in UML-SD. 4 drawn by convention as a plain arrow between a and b 5 note that we handle the UML-SD opt operator as opt(i) = alt(i, ∅) = alt(∅, i) 

• i | = i and for p = 1.p (resp. 2.p ) in pos(i), i |p = i 1|p (resp. i 2|p ).

As explained in Sec. 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 ) ∈ ord(i 1 ) and (e 2 , o 2 ) ∈ 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 ) ∈ ord(i 1 ) and (e 2 , o 2 ) ∈ ord(i 2 ), ord(i) contains (1.e 1 ∪ 2.e 2 , 1.o 1 ∪ 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 ) ∈ ord(i 1 ) and (e 2 , o 2 ) ∈ ord(i 2 ), ord(i) contains an ordering (e, o) that concerns all actions from both children i.e. e = 1.e 1 ∪ 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 ∪ 2.o 2 ∪ {(p 1 , p 2 )|p 1 ∈ 1.e 1 , p 2 ∈ 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 ∪ 2.e 2 and o = 1. 

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 α(1) ...i |e α(n) where α 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 α(j)

The semantics σ(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) ∈ ord(i). 

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 loop seq (the classical loop), loop strict and loop par . 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 par and loop strict in addition to the classic loop seq improves expressiveness. In rough terms, loop par always allows new instantiations as each instance is executed in parallel w.r.t each others and the loop itself. loop strict on the contrary does not allow new instantiations as long as the previous instance has not been entirely executed. The behavior of loop seq 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 B(L, M ) to I(L, M )). As in Def.6, any time we do so, we will only define the missing cases concerning loop terms. 

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 = seq(a!m, b?m), we have i[c?m] 2 = seq(a!m, c?m). This notation is convenient to represent terms obtained by loop unfolding. For example let us consider an interaction i ∈ I(L, M ) with a loop seq at a position p ∈ pos(i), that is, such that i |p = loop seq (i |p.1 ). The interaction is then obtained from i by unfolding once the loop at position p is i[seq(i |p.1 , i |p )] p . In Def.7, the set Υ (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 

We define a function F : I(L, M ) → B(L, M ) that flattens interactions with loops i.e. that replaces all loop subterms with the empty interaction ∅. For instance, in Fig.4 we have F (i) = ∅ and F (i ) = seq(i |1 , ∅). As F (I(L, M )) ⊂ B(L, M ), we can define an unfolding-based semantics 7 for i ∈ I(L, M ) by simply considering the union of semantics obtained from flattened unfoldings of i.

We define σ u : I(L, M ) → P(Act(L, M ) * ) such that for all i in I(L, M ):

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 ∈ σ u (i). Naturally, being able to do so without having to compute σ u (i) is preferable. In the following we'll refer to this problem as 'trace analysis'. 

. Even if feasible, this would be time and space consuming 8 . As for non acceptation, it equates to proving

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 (σ o ) whose description is the purpose of Sec.3.

σ 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 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 7 coined σu, u standing for 'unfolding-based' 8 • If the last interaction i n can express the empty trace (i.e. ∈ σ u (i n )) -which can be statically analysed -then t is accepted by i i.e. t ∈ σ o (i).

• In any case, for all frontier actions act n+1 of i n , we have i n actn+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

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 ∀j ∈ {1, 2} * , p.j ∈ 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. ∀p ∈ e we have (p , p) ∈ 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 (∅, ∅) corresponds to the case where the loop has not unfolded. According to this, the frontier of i from {p ∈ e | ∀p ∈ e, (p , p) ∈ o}

The design of the rules i act − − → i hinted at earlier is made operational thanks to 2 mechanisms: pruning and execution. Given an action act ∈ f ront(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 . 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| 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 [∅] .

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 Θ(act) = l, the current branch must be pruned so prune(act, l) = (∅, ): the value of the returned interaction i has no importance here because a parent will be pruned anyway. If Θ(act) = l we have prune(act, l) = (act, ⊥) because there is nothing to prune here. Similarly, we have prune(∅, l) = (∅, ⊥).

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 ∈ {strict, seq, par}, if any one child must be pruned (b 1 ∨ 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 ∅ 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 loop f (i 1 ). 

Let us consider the example i from Fig.6 . We wish to execute the frontier action i |22 = a!m 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. ∃p ∈ {1, 2} * s.t. p = p 0 .2.p and s.t. i |p0 = seq(i |p0.1 , i |p0.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 χ (Def.12), which takes as arguments an interaction i and a frontier position p and returns the remaining interaction i . As explained earlier, χ orchestrates the use of prune. In the example from When an alt node is reached, using the same notations, we would have:

. 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 |d1...dj = loop f (i |d1...dj .1 ) (with a mandatory d j+1 = 1), we have :

. Indeed, the execution is done on a copy of the loop content that precedes (with f operator) the loop i |d1...dj 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 |d1...dj = seq(i |d1...dj .1 , i |d1...dj .2 ) and d j+1 = 2, when constructing χ(i |d1...dj , d j+1 ...d n ) we must prune in i |d1...dj .1 all the actions that could interfere with i |p i.e. those taking place on Θ(i |p ). As such, given (i 1 , b 1 ) = prune(i |d1...dj .1 , Θ(i |p )), we'll replace the left branch of the seq with i 1 and reconstruct:

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 |d1...dj = strict(i |d1...dj .1 , i |d1...dj .2 ) and d j+1 = 2: 

In Def.13 below, we now define the operational semantics. Note that interactions that can express the empty trace are identified with the predicate exp . This semantics expresses rules of the form i

We define σ o : I(L, M ) → P(Act(L, M ) * ) as:

with empty(i) = { } (resp.∅) if exp (i) = (resp. ⊥) where exp : I(L, M ) → bool is defined as: Experiments. We implemented both semantics (σ u from Def.8 and σ o from Def.13) and compared the set of traces σ u (i) and σ 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 σ u (i) = σ 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. We define an ω 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 ∈ σ o (i); • T ooShort is returned when t ∈ σ o (i) is a strict prefix of a trace of i i.e. ∃t ∈ Act(L, M ) * s.t. t.t ∈ σ o (i); • T ooLong is returned when neither Covered nor T ooShort can be, and given t = act 1 ...act n ∃k < n s.t. act 1 ...act k ∈ σ 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 V erdict and provide it with a total order Out ≺ T ooLong ≺ T ooShort ≺ Covered.

• If t is empty then: either i accepts the empty trace in its semantics and in this case ω(i, t) returns Covered, or it returns T ooShort. ω(i, ) = Covered (resp. T ooShort) if exp (i) = (resp. ⊥) if t is of the form act.t then: Each of those traces were tested as well as a random selection of their prefixes and of interesting mutants. Addition (resp. replacement) mutants consists in adding an action to a trace (resp. prefix). By construction we could classify all those traces according to the verdicts they are expected to obtain. Fig.9 details those results, showing a systematic concordance between the expected and obtained verdicts. Those results reinforce our confidence on ω, the more so that they were done on a panel of traces and interactions which covers all 2 by 2 combinations of operators.

To provide an evaluation of performances (plotting time vs. length), we needed a large model and long correct traces. Indeed, the time required by the analysis is not always correlated to trace length e.g. an arbitrarily long trace starting with an action act of position p ∈ f ront(i) is analyzed immediately, whatever length it may be. There is however a correlation for correct traces and their prefixes. We defined a partial high-level model of the MQTT [22] telecommunication protocol (see Fig.10-a) . This model states that a communication session between a client and a broker starts (resp. ends) with a sequential connection (resp. disconnection) phase. In between, at any time, any number of instances of one of the 5 proposed subinteractions can be run concurrently. Hence, we used a multithreaded Python script to generate 100 traces, each of those corresponding to the concurrent activation and execution at random time intervals of 20 instances of the loop par from Fig.10 -a. All those traces (resp. prefixes) have the verdict Covered (resp. T ooShort); we evaluated computation times and plotted some of them on Fig.10 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 par ) operators and by the fact that messages are not uniquely identified. For instance analyzing t = a!m.b?m on i = par(a!m, strict(a!m, b?m)) would give rise to 2 branches: i = strict(a!m, b?m) (resp. i = par(a!m, 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.

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 ↓ (the empty process terminates) and a a − → (a being an atomic action), an expression describing a MSC is build using rules such as (x a − → x ) ∧ (y a − →) ⇒ (x ∓ y 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 syntactic term transformations. Still, it also requires a communication medium as it is defined as the output of a combination of two transitions systems: an execution 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 mechanisms between lifelines, several approaches that aim to implement tools, impose synchronisation points when entering and exiting combined operators and at decision 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 allowing 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.

In this paper we proposed an operational semantics for ILs, aimed at trace validity 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 relations allow the identification of immediately executable actions. Pruning techniques 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 concurrently 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 operators 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 translationbased approaches. This may consist in a comparison of formal semantics and/or in benchmarking implementations according to a certain performance metric.

Model checking of message sequence charts

Eliciting unitary constraints from timed sequence diagram with symbolic techniques: Application to testing

Software Engineering Conference

An institution for uml 2.0 interactions

Tree automata techniques and applications

Automatic model transformation from uml sequence diagrams to coloured petri nets

Lscs: Breathing life into message sequence charts

Handbook of theoretical computer science

Compositional semantics for uml 2.0 sequence diagrams using petri nets

A hierarchy of communication models for message sequence charts

A toolset for conformance testing against uml sequence diagrams based on event-driven colored petri nets

Timed sequence diagrams and tool-based analysis -A case study

Papyrus: A UML2 Tool for Domain-Specific Language Modeling

Assert and negate revisited: Modal semantics for UML sequence diagrams

STAIRS towards formal design with sequence diagrams

An end-to-end framework for safe software development. Microprocessors and Microsystems 62

Coloured Petri Nets and CPN Tools for modelling and validation of concurrent systems

UML Interactions Meet State Machines -An Institutional Approach. In: 7th Conf. on Algebra and Coalgebra in Computer Science

Uppaal in a nutshell

Global and local testing from message sequence charts

A fully general operational semantics for uml 2.0 sequence diagrams with potential and mandatory choice

The many meanings of uml 2 sequence diagrams: a survey

OMG: Unified Modeling Language v2

An operational semantics for CSP

High-level message sequence charts

Operational semantics for msc

Semantics of interactions in uml 2.0. In: IEEE Symposium on Human Centric Computing Languages and Environments

Termos: A formal language for scenarios in mobile computing systems

), 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