Runtime verification is a lightweight formal verification technique that checks the correctness of the behaviour of a system. A problem with this technique is that most monitoring specification languages are not actually used in practice by system designers. To avoid this problem, we propose an monitoring approach on basis of an extension of live sequence charts (LSCs). We extend the standard LSCs as proposed by Damm and Harel by introducing the notation of “sufficient prechart”, and by adding concatenation and product of charts. In this approach, a monitor solves the word problem that whether an observed behaviour of the underlying system is accepted by an extended LSC (eLSC) property. An on-line monitoring algorithm will be presented in the full version of the paper.
Runtime verification [
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 [
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. 2
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 2 . 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 bS , fm:sendjm 2 g as the set of send labels, the set bR , fm:recvjm 2 g as the set of receive lables, and b , bS [ bR the set of event labels. A trace over b is an element of b . The length of is j j.
A lifeline l is a (possible empty) sequence of labels l , (e^1; :::; e^n). A basic chart c is a (possible empty) set of lifelines c , fl1; :::; lng. Let Z 0 be the set of positive integer. An event e in a basic chart is a tuple e , (e^; x1; x2) with x1; x2 2 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) 7! Z 0 that maps an event to the index of the lifeline on which it occurs; 2. a bijective mapping f : S 7! R between sending and receiving events, matching a sending event to its corresponding receiving events. 3. a mapping lab : E (c) 7! b maps an event e to its label, i.e., lab(e) , e^.
The chart c induces a partial relation on E (c) as follows. 1. for any 1 xi jcj and 1 xj < jlxij, it holds that (e^; xi; xj) (e^0; xi; (xj + 1)); and 2. for any s 2 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. [
Traces(c) , {(lab(ex1), lab(ex2), ..., lab(exn)) j {ex1, ex2, ..., exn} = E (c); n = jE (c)j; and for all exi, exj 2 E (c), if exi exj , then xi < xj}. Let bc , Se2E (c)flab(e)g be the set of labels appearing in c. We call each c 2 ( bn bc) a stutter label. For each basic chart c, the language L(c) is defined by L(c) , {( c , e1, c , e2, ..., c , en, c )g, where (e1 e2, ..., en) 2 Traces(c) and each c is a finite (or empty) sequence of stutter labels. A trace is admitted by a basic chart c (denoted by c) if 2 L(c).
(b) c2: non-degeneracy (c) c3: degeneracy
(d) Partial Order induced by c1 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 2 fNec; Su g 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 2 bn( bp [ bm) . 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 L0, let (L L0) be the concatenation of L and L0 (i.e., (L L0 , f( 0) j 2 L and 0 2 L0)); and L be the complement of L (i.e., for any 2 b , it holds that 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 = Su .
This formalizes the intuitive interpretation given above. An eLSC specification U is a finite set of eLSCs. The language of U is L(U) , T L(u). u2U 4
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 c0, denoted with (c ! c0). Intuitively, a trace composed of two segments and 0 is in the language of (c ! c0) if and only if and 0 are admitted by c and c0, respectively. Formally, the language of (c ! c0) is
L(c ! c0) ,
L(c) \ L(c0) \ L(c) L(c0) .
Since an eLSC u consists of two basic charts p and m, there are four possibilitites to define the ocncatenation of eLSCs u and u0: (p ! p0), (p ! m0), (m ! p0) and (m ! m0).
The concatenation of u and u0 is defined to be a tuple , (u; u0; Mode), where Mode 2 fpp; pm; mp; mmg. Formally, the semantics of is given as follows.
Definition 3. Given two eLSCs u and u0, the language of , (u; u0; Mode) is
L( ) ,
L(u) \ L(u0) \ L(c) L(c0) , where c = p and c0 = p0, if Mode = pp; c = p and c0 = m0, if Mode = pm; c = m and c0 = p0, if Mode = mp; and c = m and c0 = m0, if Mode = mm.
It can be shown that the language of is the same as the language of the eLSC specification fu, u0, (c, c0, su )g, where the values of c and c0 are assigned according to Mode.
We recall the definition of the product LjjL0 of two languages L and L0 of traces.
A label transition system is a tuple S , (Q; qini; qfin; b; R), where – Q is a (non-empty) finite set of states; – qini – qfin 2 S is the initial state;
2 S is the final state; – b is a finite set of labels; and – R Q b Q is a finite set of binary relations. Each triple (q; e; q0) 2
R is called a transition.
Given a transition r = (q; e; q0) 2 R, we write A(r) , e for the label of r, and we write Pre(r) , q and Post(r) , q0 for the predecessor state and successor state of r, respectively. A finite trace , (e1; :::en) over b is accepted by S (denoted with j= S) if and only if there exists a sequence of transitions (r1; :::; rn) such that – Pre(r1) = qini, Post(rm) = qfin 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; r0 2 R it holds that Post(r) 6= Pre(r0), Post(r) 6= Post(r0) and Pre(r) 6= Pre(r0). 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 S1jjS2 of two label transition systems S and S0.
Definition 4. Given two label transition systems S1 , (Q1; q1ini; q1fin; b1; R1) and S2 , (Q2; q2ini; q2fin; b2; R2), the product S = (S1jjS2) is a tuple (Q; qini; qfin; b; R), where – Q , Q1 Q2; – qini , (q1ini; qini);
2 – qfin , (q1fin; q2fin); – b , b1 [ b2; – ((q1; q2); e; (q10; q20)) 2 R iff (q1; e; q10) 2 R1 and (q2; e; q20) 2 R2, or (q1; e; q10) 2 R1 and 8q20 2 Q2 : (q2; e; q20) 2= R2 and q2 = q20, or (q2; e; q20) 2 R2 and 8q10 2 Q1 : (q1; e; q10) 2= R1 and q1 = q10. We write L(S1jjS2) , f j j= (S1jjS2)g for the set of trace accepted by (S1jjS2). Given S1 , LLTS( 1) and S2 , LLTS( 2), the product of 1 and 2 is 1jj 2 , L(S1 jj S2).
The product of two languages L1 and L2 is L1jjL2 , ( 1jj 2).
S 12L1; 22L2 The language of the product (c1jjc2) of basic charts c1 and c2 is defined as follows. Definition 5. Given two basic charts c and c2 over b and the stutter label Similar as concatenations, there are four possibilities to define the product of eLSCs u1 and u2: p1jjp2, p1jjm2, m1jjp2 and m1jjm2. Definition 6. The product of two eLSCs u1 and u2 is defined to be a tuple u1jju2 , (u1; u2; Prod ), where Prod 2 fpjjp; pjjm; mjjp; mjjmg. Formally, the semantics of the four product possibilities is given as follows.
Definition 7. Given two eLSCs u1 and u2, the language of the product of u1 and u2 is L(u1jju2) , (L(u1) \ L(u2) \ L(c1jjc2)), where c = p and c0 = p0, if Prod = p||p; c = p and c0 = m0, if Prod = p||m; c = m and c0 = p0, if Prod = m||p; and c = m and c0 = m0, if Prod = m||m.