Intorduction

Runtime verification [3] is proposed for checking whether the behaviour of a system satisfies a correctness property. When compared to model checking and traditional testing, it is seen as a lightweight formal verification technique. Unlike model checking, runtime verification does not check all executions of the underlying system, but a finite trace. Therefore, it is able to avoid the so-called state explosion problem in model checking. When runtime verification is employed in the real system, it can be understand as ongoing testing. This makes the verification complete in a certain sense [4]. Such implementations are termed online monitoring, where a monitor checks the current execution of a system. Runtime verification is performed by using a monitor. A monitor is device or a piece of software that consists of a correctness property and a checking algorithm. It reads an execution of the underlying system and reports whether the execution meets the property. An execution observed by a monitor is presented by a trace, which is a sequence of events. The correctness property of a monitor is typically specified by various temporal logic (e.g., linear temporal logic (LTL), metric temporal logic (MTL), time propositional temporal logic (TPTL) and first-order temporal logic (LT L F O )), regular expressions and context-free languages.

Although these languages are expressiveness and technically sound for monitoring, they are not (yet) actually used in practice by system designers. Graphical languages such as message sequence charts (MSCs) and UML sequence diagrams (UML-SDs) are widely used in industry for system specifications. Unfortunately, as semi-formal languages, the semantics of MSC and UML-SD is not defined formally. One of the central problems in these languages is that these languages cannot distinguish between necessary (i.e., enforced) and possible (i.e., allowed) behaviours. Since there does not seem to be an solution on this problem, these languages are not suitable for specifying monitoring correctness properties. In this paper, we investigate the use of live sequence charts (LSCs) as proposed by Damm and Harel [2] for monitoring specifications. The LSC language is an extension of MSC. It specifies the exchange of messages among a set of instances. Using the notations of universal and existential chart, it can express that a behaviour of a system is necessary or possible. A universal chart specifies a necessary behaviour, whereas an existential chart specifies a possible behaviour. For monitoring, we focus on universal charts. A universal chart typically consists of two components (basic charts): a prechart and a main chart. The intended meaning is that if the prechart is executed (i.e., the underlying system exhibits an execution which meets the prechart), then the main chart must be executed afterwards. The standard definition thus interprets the prechart as a necessary condition for the main chart. For monitoring it is also important to express sufficient conditions of statements (e.g., absence of unsolicited responses). Unfortunately, sufficient conditions of statements cannot be expressed by a finite set of negation-free universal LSCs. Since the semantics of negative LSCs is hard to define, we extend LSCs to eLSCs by introducing the notion of a "sufficient" prechart for specifying this case. In contrast, we call the prechart of a standard universal chart a "necessary" prechart. With this extension, one can easily and intuitively express situations as above. In our previous work, we made an assumption: every message appearing in an eLSC is unique. Although this assumption makes sense in practical work (e.g., every message is unique with a unique time stamp), it is considered to be very strong in theoretical work. In this extended abstract, we release this restriction in the eLSC language. An eLSC based monitor essentially solves the well-known word problem: whether an observed trace is accepted by the language of an eLSC property. An on-line monitoring algorithm for this problem will be presented in the full version of the paper.

Definition of Basic Charts

We first define a basic chart of an eLSC. A basic chart is visually similar to an MSC. It contains a set of messages and a set of lifelines. When a basic chart is executed, for each message two events occurs: the event of sending the message and the event of receiving it. The partial order of events induced by a basic chart is as follows.

an event at a higher position in a lifeline precedes an event at a lower position in the same lifeline; and for each message m, the send-event of m precedes the receive-event of m. Formally, a basic chart can be defined as follows. Let Σ be a finite alphabet of messages m, i.e., m ∈ Σ. We use the labels m.send and m.recv to denote the event of sending a message m and the event of receiving m, respectively. We define Σ S {m.send|m ∈ Σ} as the set of send labels, the set Σ R {m.recv|m ∈ Σ} as the set of receive lables, and Σ Σ S ∪ Σ R the set of event labels. A trace τ over Σ is an element of Σ * . The length of τ is |τ |. A lifeline l is a (possible empty) sequence of labels l (ê1, ..., ên). A basic chart c is a (possible empty) set of lifelines c {l1, ..., ln}. Let Z ≥0 be the set of positive integer. An event e in a basic chart is a tuple e (ê, x1, x2) with x1, x2 ∈ Z ≥0 , where x1 is the index of the lifeline on which e occurs, and x2 is the index of the position of the lifeline where e occurs. Each event of a basic chart is unique. We denote the set of events appearing in c with E (c). The set E (c) can be partitioned into a set S of sending events and a set R of receiving events, i.e., E (c) = S ∪ R. Given a basic chart c over an alphabet Σ, we define the following mappings.

1. a mapping p : E (c) → Z ≥0 that maps an event to the index of the lifeline on which it occurs; 2. a bijective mapping f : S → R between sending and receiving events, matching a sending event to its corresponding receiving events. 3. a mapping lab : E (c) → Σ maps an event e to its label, i.e., lab(e) ê. The chart c induces a partial relation on E (c) as follows.

1. for any 1 ≤ xi ≤ |c| and 1 ≤ xj < |lxi|, it holds that (ê, xi, xj) ≺ (ê , xi, (xj + 1)); and 2. for any s ∈ S , it holds that s ≺ f (s). 3. ≺ is the smallest relation satisfying 1. and 2. We admit the non-degeneracy assumption proposed by Alur et. al. [1]: a basic cannot reverse the receiving order of two identical messages sent by some lifeline. Formally, a basic chart is degeneracy if and only if there exist two sending events e1, e2 ∈ S such that lab(e1) = lab(e2) and e1 ≺ e2 and f (e1) ≺ f (e2). For instance, in fig. 1

Extended LSCs

A universal chart consists of two basic charts: a prechart and a main chart (drawn within a solid rectangle). For an eLSCs, there are two possibilities of the prechart: a necessary prechart (drawn within surrounding hashed hexagons) or a sufficient prechart (dran within surrounding solid hexagons). Formally, the syntax of eLSCs is as follows.

Definition 1. An eLSC is a tuple u (p, m, Cond), where p and m are a prechart and a main chart, and Cond ∈ {Nec, Suff } denotes if p is a necessary or sufficient prechart.

We define an althernative semantics of eLSCs. On one hand, an eLSC with a necessary prechart intuitively specifies all traces composed of two segments such that, if the first segment is admitted by the prechart, then the second must be admitted by the main chart. On the other hand, an eLSC with a sufficient prechart specifies all traces composed of two segments such that, the first segment cannot be admitted by the prechart, unless the second is admitted by the main chart. Given an eLSC u = (p, m, Cond), the stutter labels of u are σu ∈ Σ\( Σp ∪ Σm) . The language L(p) of the prechart (resp. the language L(m) of the main chart) is defiend with T races(p) (resp. T races(m)) and these stutter labels as above.

For languages L and L , let (L • L ) be the concatenation of L and L (i.e., (L • L {(τ τ ) | τ ∈ L and τ ∈ L )); and L be the complement of L (i.e., for any τ ∈ Σ * , it holds that τ ∈ L iff τ / ∈ L). The alternative semantics of eLSCs is defined as follows.

Definition 2. Given a finite alphabet Σ, the language of an eLSC u (p, m, Cond) is

L(u) L(p) • L(m), if Cond = Nec; and L(u) L(p) • L(m), if Cond = Suff .

This formalizes the intuitive interpretation given above. An eLSC specification U is a finite set of eLSCs. The language of U is L(U) u∈U L(u).

Concatenations of eLSCs

Concatenation of two eLSCs essentially introduces partial orders of executions of the charts. This feature can be inherited by eLSC specifications. We first define the concatenation of basic charts c and c , denoted with (c → c ). Intuitively, a trace composed of two segments υ and υ is in the language of (c → c ) if and only if υ and υ are admitted by c and c , respectively. Formally, the language of (c → c ) is

L(c → c ) L(c) ∩ L(c ) ∩ L(c) • L(c ) .

Since an eLSC u consists of two basic charts p and m, there are four possibilitites to define the ocncatenation of eLSCs u and u : (p → p ), (p → m ), (m → p ) and (m → m ).

The concatenation of u and u is defined to be a tuple δ (u, u , Mode), where Mode ∈ {pp, pm, mp, mm}. Formally, the semantics of δ is given as follows.

Definition 3. Given two eLSCs u and u , the language of δ (u, u , Mode) is It can be shown that the language of δ is the same as the language of the eLSC specification {u, u , (c, c , suff )}, where the values of c and c are assigned according to Mode.

L(δ) L(u) ∩ L(u ) ∩ L(c) • L(c

We recall the definition of the product L||L of two languages L and L of traces. A label transition system is a tuple S (Q, q ini , q f in , Σ, R), where -Q is a (non-empty) finite set of states; q ini ∈ S is the initial state; q f in ∈ S is the final state; -Σ is a finite set of labels; and -R ⊆ Q× Σ×Q is a finite set of binary relations. Each triple (q, e, q ) ∈ R is called a transition. Given a transition r = (q, e, q ) ∈ R, we write A(r) e for the label of r, and we write Pre(r) q and Post(r) q for the predecessor state and successor state of r, respectively. A finite trace τ (e1, ...en) over Σ is accepted by S (denoted with τ |= S) if and only if there exists a sequence of transitions (r1, ..., rn) such that -Pre(r1) = q ini , Post(rm) = q f in and for all 0 ≤ i < m it hold that Post(ri) = Pre(ri+1); and -(A(r1), ..., A(rm)) = τ . We say a label transition system is linear if and only if for all r, r ∈ R it holds that Post(r) = Pre(r ), Post(r) = Post(r ) and Pre(r) = Pre(r ). It can be shown that there exists only one trace accepted by a linear label transition system. For a linear label transition system S and the trace τ accepted by S, we define LLTS(τ ) S. The product of two traces τ1 and τ2 can then be defined with the product of LLTS(τ1) and LLTS(τ2). Now we define the product S1||S2 of two label transition systems S and S . Definition 4. Given two label transition systems S1 (Q1, q ini 1 , q f in 1 , Σ1, R1) and S2 (Q2, q ini 2 , q f in 2 , Σ2, R2), the product S = (S1||S2) is a tuple (Q, q ini , q f in , Σ, R), where -Q Q1 × Q2; q ini (q ini 1 , q ini 2 ); q f in (q f in 1 , q f in 2 ); -Σ Σ1 ∪ Σ2; -((q1, q2), e, (q 1 , q 2 )) ∈ R iff

• (q1, e, q 1 ) ∈ R1 and (q2, e, q 2 ) ∈ R2, or • (q1, e, q 1 ) ∈ R1 and ∀q 2 ∈ Q2 : (q2, e, q 2 ) / ∈ R2 and q2 = q 2 , or • (q2, e, q 2 ) ∈ R2 and ∀q 1 ∈ Q1 : (q1, e, q 1 ) / ∈ R1 and q1 = q 1 .

We write L(S1||S2) {τ | τ |= (S1||S2)} for the set of trace accepted by (S1||S2). Given S1 LLTS(τ1) and S2 LLTS(τ2), the product of τ1 and τ2 is τ1||τ2 L(S1 || S2). The product of two languages L1 and L2 is L1||L2

τ 1 ∈L 1 ,τ 2 ∈L 2 (τ1||τ2).

The language of the product (c1||c2) of basic charts c1 and c2 is defined as follows.

Definition 5. Given two basic charts c and c2 over Σ and the stutter label σ ∈ Σ\( Σc 1 ∪ Σc 2 ) , the language of c1||c2 is L(c1||c2) {(σ * , e1, σ * , e2, ..., σ * , en, σ * ) | (e1, e2, ..., en) ∈ (Traces(c1 ) || Traces(c2 ))} Similar as concatenations, there are four possibilities to define the product of eLSCs u1 and u2: p1||p2, p1||m2, m1||p2 and m1||m2.

Definition 6. The product of two eLSCs u1 and u2 is defined to be a tuple u1||u2 (u1, u2, Prod ), where Prod ∈ {p||p, p||m, m||p, m||m}.

Formally, the semantics of the four product possibilities is given as follows.