System Monitoring with Extended Message Sequence Chart (Extended Abstract)? Ming Chai Institut für Informatik Humboldt Universität zu Berlin ming.chai@informatik.hu-berlin.de Abstract. Runtime verification is a lightweight formal verification tech- nique 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 prob- lem, 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. 1 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 veri- fication technique. Unlike model checking, runtime verification does not check all executions of the underlying system, but a finite trace. There- fore, 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 de- vice 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 ob- served 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 tem- poral logic (LT LF O )), regular expressions and context-free languages. ? This work was supported by the State Key Laboratory of Rail Traffic Control and Safety (Contract No.: RCS2012K001), Beijing Jiaotong University Although these languages are expressiveness and technically sound for monitoring, they are not (yet) actually used in practice by system de- signers. 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 under- lying 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, suf- ficient 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 con- sidered 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 prop- erty. An on-line monitoring algorithm for this problem will be presented in the full version of the paper. 2 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 Σ b S , {m.send|m ∈ Σ} as R b , {m.recv|m ∈ Σ} as the set of receive the set of send labels, the set Σ lables, and Σ b,Σ bS ∪ Σb R the set of event labels. A trace τ over Σb is an element of Σ b ∗ . 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) 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) , ê. 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) ≺ (ê0 , 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 ) 6≺ f (e2 ). For instance, in fig. 1 (a) - (c), the basic charts c1 and c2 are non-degeneracy, whereas c3 is degeneracy. The basic chart c3 cannot distinguishes between the two receiving events of m1. The partial order of the labels induced by the basic chart c1 is shown as in fig 1(d). A set of traces over Σ b is defined by c as follows: Traces(c) , {(lab(ex1 ), lab(ex2 ), ..., lab(exn )) | {ex1 , ex2 , ..., exn } = E (c); n = |E (c)|; and for all exi , exj ∈ E (c), if exi ≺ exj , then xi < xj}. S Let Σ e∈E (c) {lab(e)} be the set of labels appearing in c. We call bc , each σc ∈ (Σ\ b Σ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∗ )}, where (e1 e2 , ..., en ) ∈ 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 τ ∈ L(c). (a) c1: non-degeneracy (b) c2: non-degeneracy (c) c3: degeneracy (d) Partial Order induced by c1 Fig. 1. Example:Degeneracy in Basic Charts 3 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 pos- sibilities 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. Givenan eLSC u =  (p, m, Cond), the stutter labels of u are σu ∈ Σ\(Σp ∪ Σm ) . The language L(p) of the prechart (resp. the lan- b b b guage 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 , {(τ τ 0 ) | τ ∈ L and τ 0 ∈ L0 )); and L be the complement b ∗ , it holds that τ ∈ L iff τ ∈ of L (i.e., for any τ ∈ Σ / 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 eLSCT speci- fication U is a finite set of eLSCs. The language of U is L(U) , L(u). u∈U 4 Concatenations of eLSCs Concatenation of two eLSCs essentially introduces partial orders of ex- ecutions of the charts. This feature can be inherited by eLSC specifica- tions. 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 ∈ {pp, pm, mp, mm}. 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 {u, u0 , (c, c0 , suff )}, where the values of c and c0 are assigned according to Mode. 5 Product of eLSCs We recall the definition of the product L||L0 of two languages L and L0 of traces. A label transition system is a tuple S , (Q, q ini , q f in , Σ, b 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; – Σb is a finite set of labels; and – R ⊆ Q×Σ×Q b is a finite set of binary relations. Each triple (q, e, q 0 ) ∈ R is called a transition. Given a transition r = (q, e, q 0 ) ∈ R, we write A(r) , e for the label of r, and we write Pre(r) , q and Post(r) , q 0 for the predecessor state and successor state of r, respectively. A finite trace τ , (e1 , ...en ) over Σ b 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, r0 ∈ 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 S1 ||S2 of two label transition systems S and S0. Definition 4. Given two label transition systems S1 , (Q1 , q1ini , q1f in , Σb1 , R1 ) and S2 , (Q2 , q2ini , q f in , Σ 2 b2 , R2 ), the prod- ini f in b uct S = (S1 ||S2 ) is a tuple (Q, q , q , Σ, R), where – Q , Q1 × Q2 ; – q ini , (q1ini , q2ini ); – q f in , (q1f in , q2f in ); – Σ b,Σ b1 ∪ Σ b2 ; – ((q1 , q2 ), e, (q10 , q20 )) ∈ R iff • (q1 , e, q10 ) ∈ R1 and (q2 , e, q20 ) ∈ R2 , or • (q1 , e, q10 ) ∈ R1 and ∀q20 ∈ Q2 : (q2 , e, q20 ) ∈ / R2 and q2 = q20 , or 0 0 0 • (q2 , e, q2 ) ∈ R2 and ∀q1 ∈ Q1 : (q1 , e, q1 ) ∈ / R1 and q1 = q10 . 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 ). S The product of two languages L1 and L2 is L1 ||L2 , (τ1 ||τ2 ). τ1 ∈L1 ,τ2 ∈L2 The language of the product (c1 ||c2 ) of basic charts c1 and c2 is defined as follows.  5. Given two basic charts c and c2 over Σ and the stutter Definition b label σ ∈ Σ\( b Σ bc1 ∪ Σ bc2 ) , 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 prod- uct 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 fol- lows. Definition 7. Given two eLSCs u1 and u2 , the language of the product of u1 and u2 is L(u1 ||u2 ) , (L(u1 ) ∩ L(u2 ) ∩ L(c1 ||c2 )), 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. References 1. Rajeev Alur, Kousha Etessami, and Mihalis Yannakakis. Inference of Message Sequence Charts. Software Engineering, IEEE Transactions on, 29(7):623–633, 2003. 2. Werner Damm and David Harel. LSCs: Breathing Life into Message Sequence Charts. Formal Methods in System Design, 19(1):45–80, 2001. 3. Klaus Havelund and Grigore Roşu. Monitoring Java Programs with Java PathExplorer. Electronic Notes in Theoretical Computer Sci- ence, 55(2):200–217, 2001. 4. Martin Leucker and Christian Schallhart. A Brief Account of Run- time Verification. The Journal of Logic and Algebraic Programming, 78(5):293–303, 2009.