=Paper=
{{Paper
|id=Vol-1269/paper301
|storemode=property
|title=System Monitoring with Extended Message Sequence Chart (Extended Abstract)
|pdfUrl=https://ceur-ws.org/Vol-1269/paper301.pdf
|volume=Vol-1269
|dblpUrl=https://dblp.org/rec/conf/csp/ZbrzeznyZ14a
}}
==System Monitoring with Extended Message Sequence Chart (Extended Abstract)==
https://ceur-ws.org/Vol-1269/paper301.pdf
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.