Runtime verification is a lightweight verification technique that checks whether an execution of a system satisfies a given property. A problem in monitoring specification languages is to express parametric properties, where the correctness of a property depends on both the temporal relations of events, and the data carried by events. In this paper, we introduce parametrized extended live sequence charts (PeLSCs) for monitoring sequences of data-carrying events. The language of PeLSCs is extended from life sequence charts by introducing condition and assignment structures. We develop a translation from PeLSCs into the hybrid logic HL, and prove that the word problem of the PeLSCs is linear with respect to the size of a parametrized event trace. Therefore, the formalism is feasible for on-line monitoring.
Even with most advanced quality assurance techniques, correctness of complex software can never be guaranteed. To solve this problem, runtime verification has been proposed to provide on-going protection during the operational phase. Runtime Verification checks whether an execution of a computational system satisfies or violates a given correctness property. It is performed by using a monitor. This is a device or a piece of software that observes the system under monitoring (SuM) and generates a certain verdict (true or false) as the result. Compared to model checking and testing, this technique is considered to be a lightweight validation technique, since it does not try to cover all possible executions of the SuM. It detects failures of an SuM directly in its actual running environment. This avoids some problems of other techniques, such as imprecision of the model in model checking, and inadequateness of the artificial environment in testing.
An execution of a computational system checked by a monitor can be formalized
by a sequence of events. One of the challenges in building a runtime verification system
is to define a suitable specification language for monitoring properties. A monitoring
specification language should be expressive and attractive [
Over the last years, various runtime verification systems have been developed which use some form of temporal logic, including linear temporal logic (LTL), metric temporal logic (MTL), time propositional temporal logic (TPTL) and first-order temporal logic (LTLF O). Although these specification languages are expressive and technically sound for monitoring, software engineers are not familiar with them and need extensive training to use them efficiently. Therefore, many runtime verification systems support also other specification languages, such as regular expressions and context-free grammars. Unfortunately, it is difficult to specify properties for parallel systems in these languages, and they are not (yet) used in practice by system designers.
In previous work [
The eLSC-based monitoring approach so far can not handle parametric properties, where the correctness of a property depends on both the temporal relations of events and data carried by the events. One possible workaround for this shortage is to formalize each assignment of data with a unique atomic proposition. However, since the domain of data can be infinite or unknown, this approach is not sufficient in general. We extend eLSC to parametrized eLSC (PeLSC) by introducing assignment structures and condition structures.
In this paper, we model data-carrying events with parametrized events, where the data is represented by parameters. Consider a client/server system that allows clients to access a server, and consider the following properties.
(P1): If there is a log in to the server, it must be followed by a log out. (P2): A log out event can not occur, unless it is preceded by a log in.
(P3): If a client logs in to the server, it must log out within 200 sec.
For the first two properties, the monitor can observe a propositional events login and logout. The expected behaviours can be formalized by the following regular expressions L1 and L2, respectively.
L1 , Σ∗ ◦ {login} ◦ {logout} ◦ Σ∗
L2 , Σ∗ ◦ {login} ◦ {logout} ◦ Σ∗ For the property (P3), each of the login and logout events carries a client name and a time stamp. An execution of this system can be formalized by a sequence of parametrized events. Each of the propositional events carries two parameters client_id (id) and time_stamp (time). With these definitions, property (P3) can be written more formally as follows:
When the system emits a login event with (id = x) and (time = y), a logout event with (id = x′) and (time = y′) should occur afterwards, where (x′ = x) and (y′ ≤ (y + 200)).
The PeLSCs of Fig. 1 specify the three properties above. The chart (C1) is a standard LSC formalizing (P1). Property (P2) cannot be formalized with LSCs; an eLSC for it is (C2). Property (P3) involves parameters on infinite or unknown domains and thus cannot be expressed by eLSCs. A PeLSC for it is (P U ). Formal definitions being given below, we note that the language PeLSC contains variables, assignment and conditions for dealing with data-parametrized events. An assignment structure is used to store an arbitrary parameter value, and a condition structure is used to express constraints on such values. With these extensions, PeLSCs can be used for monitoring systems where events carry data.
To generate monitors, we translate PeLSCs into (a subclass of) the hybrid logic
(HL) [
(a) PeLSC for P1 (b) PeLSC for P2 (c) PeLSC for P3
A monitor essentially solves the word-problem: given a trace, decide whether the trace is in the language defined by a monitoring property. As a main result of this paper, we prove that the complexity of the word-problem of PeLSCs is linear if the propositions in the condition structures express only comparisons of parameter values. Thus, monitoring can be done on-line, while the SuM is running.
The rest of the paper is organized as follows. Section 2 outlines related work. Section 3 introduces parametrized eLSCs (PeLSCs), including their syntax and trace-based semantics. Section 4 presents a translation from PeLSCs into a subclasss of HL, and proves the complexity of the word problem of PeLSCs. Section 5 contains some conclusions and hints for future work. 2
Our extension of LSCs is inspired by the treatment of time in live sequence charts
proposed by Harel et. al. [
There are several other runtime verification approaches for handling parametrized
events. The EAGLE logic [
TraceMatches [
Another important direction of parametric monitoring is based on automata theory.
Quantified event automata [
Various extensions of LTL have been proposed for parametric monitoring. If time
is the only parameter, properties can be formalized with real-time logics such as TLTL
[
This section presents the syntax and semantics of parametrized extended LSCs (PeLSCs). The PeLSCs are interpreted over parametrized event traces, which are defined as follows.
Let Σ , {e1, e2, ..., en} be a finite alphabet of events, N , {s1, s2, ...} be a countable set of nominals and D , {d1, d2, ...} any domain (e.g., integers, strings, or reals). A parameter is a pair p , hs, di from N × D, where s is the name of p and d is the value of p.
Definition 1 (Parametrized event). Given an alphabet Σ of events, a set N of nominals and a domain D, a parametrized event is a pair w , he, Pi, where e ∈ Σ is an event and P ∈ 2N ×D is a set of parameters.
Given a parametrized event w with P , {hs1, d1i, ..., hsm, dmi}, we define Evet(w) , e, Para(w) , P and Nam(w) , {s1, ..., sm}. A parametrized event he, Pi is deterministic if each parameter name in P is unique, i.e., for all p, p′ ∈ P it holds that s 6= s′. In this paper, we assume that all parametrized events are deterministic.
Parametrized event traces basically are finite sequences of parameterized events.
(P1, P2, ..., Pn) over N × D is a finite sequence of sets of parameters, i.e., an element of (2N ×D)∗. Given Σ, N and D, a parametrized event trace τ , hσ, ρi is a pair of a finite event trace σ and a parameter trace ρ with the same length, i.e., σ ∈ Σ∗ and ρ ∈ (2N ×D)∗ and |σ| = |ρ|.
By τ [i] , hσ[i], ρ[i]i we denote the ith parametrized event of τ , where σ[i] and ρ[i] are the ith element of σ and ρ, respectively.
A universal PeLSC consists of two basic charts: a pre-chart and a main-chart. A basic chart is visually similar to an MSC. It specifies the exchange of messages among a set of instances. Each instance is represented by a lifeline. Lifelines in a basic chart are usually drawn as vertical dashed lines, and messages are solid arrows between lifelines. For each message, there are two actions: the action of sending the message and the action of receiving it. Each action occurs at a unique position in a lifeline. The partial order of actions induced by a basic chart is as follows.
– An action at a higher position in a lifeline precedes an action at a lower position in the same lifeline; and – for each message m, the send-action of m precedes the receive-action of m.
Let M be a set of messages, and let the set of events be given as Σ , (M × {!, ?}). That is, an event e is either m! (indicating that message m is sent, or m? (indicating that m is received).
A lifeline l is a finite (possibly empty) sequence of events l , (e1, e2, ..., en). A basic chart C is an n-tuple of lifelines hl1, ..., lni with li = (ei1, ..., eim). We say that an event e occurs at the location (i, j) in chart C if e = eij . An event occurrence o , (e, i, j) is a tuple consisting of an event e and the location of e. We define loc(o) , (i, j) as the location of an event occurrence o, and lab(o) , e be the event of o. We denote the set of event occurrences appearing in C with EO(C) A communication h(m!, i, j), (m?, i′, j′)i in C is a pair of two event occurrences in C representing sending and receiving of the same message m. We define mat(m!, i, j) , (m?, i, j) to match a sending event occurrence to a receiving event occurrence of the same communication. A communication does not have to be completely specified by a basic chart. That is, it is possible that only the sending event or the receiving event of a message appears in a basic chart. In addition, an event is allowed to occur multiple times in a basic chart, i.e., a basic chart can express that a message is repeatedly exchanged. However, each event occurrence is unique in a basic chart.
The partial relation induced by a chart C on EO(C) is formalized as follows. 1. for any 1 ≤ xj < |lxi| with lxi being a lifeline in C, it holds that (e, xi, xj) ≺ (e′, xi, (xj + 1)); 2. for any o ∈ S, it holds that o ≺ mat(o); and 3. ≺ is the smallest relation satisfying 1 and 2.
We admit the non-degeneracy assumption proposed by Alur et. al. [
For a basic chart, event occurrences are allowed to be absent, i.e., it is possible that only a sending event or a receiving event of a message appears in a basic chart. Each event occurrence is unique in a basic chart.
With basic charts, a universal eLSC can be defined as follows. A universal chart in the eLSCs consists of two basic charts: a main-chart (M ch, drawn within a solid rectangle) and a pre-chart (P ch). There are two possibilities of pre-charts: “necessary pre-charts” (drawn within a solid hexagon) and “sufficient pre-charts” (drawn within a hashed hexagon). These two pre-charts are interpreted as a necessary condition and a sufficient condition for a main-chart, respectively. Intuitively, a universal chart with a necessary pre-chart specifies all traces such that, if contains a segment which is admitted by the pre-chart, then it must also contain a continuation segment (directly following the first segment) which is admitted by the main chart. On the other hand, a universal chart with a sufficient pre-chart specifies all traces such that, if contains a segment which is admitted by the main-chart, then the segment must (directly) follows a prefix segment which is admitted by the pre-chart. Formally, the syntax of eLSCs is as follows.
U ch , (P ch, M ch, Cate) with Cate ∈ {Suff , Nec} denoting the category of the pre-chart. More specifically, the chart (P ch, M ch, Suff ) is with a sufficient pre-chart, and (P ch, M ch, Nec) is with a necessary pre-chart.
We define PeLSCs by introducing condition structure and assignment structure into eLSCs.
An assignment structure is comprised of a function v := s with v being a variable and s being the name of a parameter. The variable v is evaluated to the value of a parameter name p. The function is surrounded by a rectangle with a sandglass icon at the top right corner. A condition structure is comprised of a proposition prop surrounded by a rectangle. The proposition expresses the comparisons of parameter values. The notations for the assignment structure and the condition structure are shown in Fig. 2. In a PeLSC, assignment structures and condition structures combine naturally with event occurrences. Intuitively, an assignment structure stores the value of a parameter carried by the combined event occurrence; and a condition structure expresses the features of a parameter carried by the combined event occurrence. Formally, the syntax of the two structures are given as follows.
o ∈ EO(U ch) an event occurrence of U ch, v a free variable, s a nominal, and prop a proposition. An assignment structure is defined as a tuple assi , (v, s, o), where s represents the name of of a parameter. A condition structure is defined as a pair cond , hprop, oi.
(U ch, COND, ASSI), where U ch is an eLSC, and COND and ASSI are sets of condition structures and assignment structures, respectively.
There are two possible forms of propositions in condition structures, one is with free variables (denoted by prop(s1, ..., sn, v1, ..., vm)) and the other is without free variables (denoted by prop(s1, ..., sn)). These two forms are used to express relative parameter values and absolute parameter values, respectively. We divide the set COND of a PeLSC into two subsets CONDF V and CONDNF V . The subset CONDF V is comprised of the set of condition structures with propositions of the form prop(s1, ..., sn, v1, ..., vm); and the subset CONDNF V is comprised of the set of condition structures with propositions of the form prop(s1, ..., sn). It holds that (CONDF V ∩ CONDNF V ) = ∅ and (CONDF V ∪ CONDNF V ) = COND.
Given a parametrized event trace, the proposition in a condition structure hprop, oi is evaluated to a boolean value, according to the parameter values carried by events: – the nominals s1, ..., sn in prop are replaced by the values of the parameters named by s1, ..., sn carried by the event lab(o); and – the variables v1, ..., vm in prop are evaluated to the values from some event occurrences through the assignment structures assi(v1, sx1, ox1), ..., assi (vm, sxm, oxm).
In this paper, we require our PeLSCCs to satisfy an additional non-ambiguity assumption. We say a PeLSC is non-ambiguity, if for any condition structure with a proposition of the form prop(s1, ..., sn, v1, ..., vm), all free variable v1, ..., vm are evaluated to a certain value from a unique event occurrence. More formally, a PeLSC P U , (U ch, COND, ASSI) is non-ambiguity if and only if for any condition structure cond = (prop(s1, ..., sn, v1, ..., vm), o) in the set CONDF V it holds that for any vxi ∈ {v1, ..., vm} there exists an assignment structure (vxi, sxi, o′) ∈ ASSI with o′ ≺ o. With the non-ambiguity assumption, each proposition is able to be evaluated to a certain boolean value (true or false) over a deterministic parametrized event trace. To understand this assumption, consider the PeLSCs in Fig. 3. For the chart P U2, the variable v has no value since there is no assignment structure to store it. For the chart P U3, the variable v has two values stored by two assignment structures. Therefore, the condition structure cannot be evaluated to a certain boolean value for both of the two charts. For the chart P U4, the values of variables v1 and v2 are from different event occurrences.
The non-ambiguity assumption is a strong assumption. For instance, the variables v1 and v2 in the chart P U4 have certain values. However, the order of the two events !m1 and !m2, which are combined with the two assignment structures of v1 and v2, are uncertain. Since our monitors are generated by translating PeLSCs into HL, the size of the monitor is increased by expressing all possible executions of the pre-chart in the resulting formula. This will reduce the monitoring efficiency. (b) ambiguity (c) ambiguity (d) ambiguity A PeLSC (U ch, COND, ASSI) defines a parametrized language (a set of parametrized event traces) that is an extension of the propositional language (i.e., a set of event traces) defined by U ch. Intuitively, the parametrized language is comprised of all parametrized event traces such that the orders of events meets the partial order induced by U ch, and all propositions in COND are evaluated to true with the values from the parameters carried by the events. A parametrized event trace τ is admitted by a PeLSC P U if and only if τ is in the parametrized language defined by P U .
A set of sequences of event occurrences is defined by a basic chart C as follows: EOcc(C) , {(o[x1], o[x2], ..., o[xn])|{o[x1], o[x2], ..., o[xn]} = EO(C); n = |EO(C)|; and for all o[xi], o[xj] ∈ EO(C), if o[xi] ≺ o[xj], then xi < xj}.
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 language of event occurrences for eLSCs is given as follows.
fined by an eLSC U ch , (P ch, M ch, Cate) is as follows – EOcc(U ch) , EOcc(P ch) ◦ EOcc(M ch), if Cate = Suff ; – EOcc(U ch) , EOcc(P ch) ◦ EOcc(M ch), if Cate = Nec.
Given a set P = {hs1, d1i, ..., hsn, dmi} of parameters and a proposition prop(sy1, ..., syn), we define the evaluation of prop(sy1, ..., syn) over P (denoted with [[P ⊢ prop(sy1, ..., syn)]]) as follows.
true if prop(dy1, ..., dyn) is satisfied with [[P ⊢ prop(sy1, ..., syn)]] = {hsy1, dy1i, ..., hsyn, dymi} ⊆ P false otherwise
For the propositions of the form prop(sx1, ..., sxn, vy1, ..., vym) in P U , the values of the variables vy1, ..., vym are from the assignment structures ASSI(vy1, ..., vym) , {assi(vy1), ..., assi(vym)}, where assi(vyi) , (vyi, syi, o). By ac(sx1, ..., sxn, vy1, ..., vym) we denote the pair (prop(sx1, ..., sxn, vy1, ..., vym), ASSI(vy1, ..., vym)). Given a pair hP, P′i of two sets of parameters, the evaluation of the pair ac(sx1, ..., sxn, vy1, ..., vym) over hP, P′i is defined as follows. – [[hP, P′i ⊢ ac(sx1, ..., sxn, vy1, ..., vym)]] = true, if prop(dx1, ..., dxn, dy1, ..., dym) is satisfied with {(sx1, dx1), ..., (sxn, dxn)} ⊆ P′ and {(sy1, dy1), ..., (syn, dyn)} ⊆ P; – [[hP, P′i ⊢ ac(sx1, ..., sxn, vy1, ..., vym)]] = f alse, otherwise.
– σ = (lab(o[
By PTra(P U ) we denote the set of parametrized event traces defined by P B. Let E (U ch) be the set of events appearing in an eLSC. We call each ǫUch ∈ (Σ\E (U ch)) a stutter event, and Pǫ ∈ 2N D an arbitrary set of stutter parameters.
fined by a PeLSC P U is
PL(P U ) , {(ǫ∗, e1, ǫ∗, ..., en, ǫ∗), (Pǫ∗, P1, Pǫ∗..., Pn, Pǫ∗)}, where ((e1, ..., en), (P1, ..., Pn)) ∈ P T ra(P U ), and |(ǫ∗, e1, ǫ∗, ..., en, ǫ∗)| = |(Pǫ∗, P1, Pǫ∗..., Pn, Pǫ∗)|, and ǫ∗ and Pǫ∗ are finite (possible empty) sequences of stutter events and stutter parameters, respectively. 4
In this subsection, we present a translation of PeLSCs into a subclass of the hybrid logic (HL) formulae. Whether an observation is admitted by a PeLSC can then be checked with the resulting formula.
The syntax and semantics of HL are given as follows.
Definition 8 (Syntax of HL). Given the finite set AP of atomic propositions, a set V of variables, the set Z of integers, and a set N of nominals, the terms π and formulae ϕ of HL are inductively formed according to the following grammar, where x ∈ V , p ∈ AP , s ∈ N , r ∈ Z and ∼∈ {<, =}: π ::= x + r | r ϕ ::= ⊥ | p | (ϕ1 ⇒ ϕ2) | (ϕ1 U ϕ2) | (π1 ∼ π2) | x ↓ s.ϕ.
Intuitively, an HL formula x ↓ s.ϕ(x) is satisfied by a parametrized event trace
τ , (σ, ρ) if and only if ϕ(d) is satisfied by σ with (s, d) ∈ ρ[
Assume that E is a function E : V → Z for assigning free variables in the domain of integers N≥0 such that E (x + d) = E (x) + d and E (d) = d. Given a variable x and a natural number d, we denote E [x := d] for the evaluation E ′ such that E ′(x) = d, and E ′(y) = E (y) for all y ∈ V \{x}. The HL is defined on parametrized event traces as follows.
Let τ , (σ, ρ) be a parametrized event trace with σ , (e[
As usual, τ |= ϕ iff (τ, 1, E ) |= ϕ.
We now show how to translate a PeLSC into an HL formula to check whether a
parametrized trace is admitted. The translation is developed on basis of the translation
form an eLSC U ch into an LTL formulae ϕ(U ch) as shown in [
A PeLSC is comprised of a universal eLSC U ch, a set COND of condition structures and a set ASSI of assignment structures. Propositions appearing in a PeLSC are specified by the comparisons of terms, i.e., π1 ∼ π2. According to the subset CONDNF V and CONDF V , the following formulae are defined.
– Let e be an even in U ch combined with a constraint structure cond = (prop, o from the set CONDNF V with prop(s1, ..., sn) and lab(o) = e. The condition structure is translated into an HL formula d(cond) ,
(x1 ↓ s1. · · · xn ↓ sn.(e ⇒ prop(x1, ..., xn))).
The formula specifies that whenever the event e occurs, then the proposition must be evaluated to true with values of the parameters named by s1, ..., sn carried by e. I.e., if the event occurs at a position z1 of the trace, the proposition prop(d1, ..., dn) is true with {(s1, d1), ..., (sn, dn)} ⊆ ρ[z1]. d(cond) , ((e′ ∧ ♦e) ⇒ (x1 ↓ v1. · · · xm ↓ vm.(e′ ∧ ♦y1 ↓ s1. · · · yn ↓
sn.(e ∧ (prop(y1, ..., yn, x1, ..., xm)))))).
This formula expresses that if both of the events, combined with the assignment structures and with the condition structure, occurs, then the proposition must be evaluated to true with the values of the parameters carried by the two events. I.e., if e′ and e occur at positions z1 and z2 of the trace, respectively, the proposition prop(dzy1, ..., dzyn, dzx1, ..., dzxm) is true with {(szy1, dzy1), ..., (szyn, dzyn)} ⊆ ρ[z2] and {(szx1, dzx1), ..., (szxm, dzxm)} ⊆ ρ[z1].
From a PeLSC P U , (U ch, COND, ASSI) we define an HL formula ϕ(P U ) , ϕ(U ch) ∧
V cond∈CONDNF V d(cond) ∧
V cond∈CONDF V
! d(cond) .
The formula expresses that, a parametrized event trace τ = (σ, ρ) satisfies the formula ϕ(P U ) if and only if σ is in the language defined by U ch, and the parameters carried by the events in τ meet the specification of the assignment structures and the condition structures. For any parametrized event trace τ , it holds that τ is admitted by P U iff τ |= ϕ(P U ).
A rewriting algorithm for HL can be developed directly upon the semantics of the
logic. Then a PeLSC property can be checked by a monitor by implementing the
algorithm in some rewriting environment, e.g, Maude [
Theorem 1. The complexity of the word-problem of HL is linear with respect to the size of input traces.
Proof. Given an HL formula ϕ = x ↓ s.ψ(x) and a parametrized event trace τ ,
(σ, ρ). The trace τ satisfies ϕ if and only if σ |= ψ(d) with (s, d) ∈ ρ[
Corollary 1. The complexity of PeLSCs is linear with respect to the size of traces.
According to the corollary, the language of PeLSCs is feasible for runtime verification implementations, especially for on-line monitoring.
We implement the algorithms in Maude [
(b) Temporal requirements In this paper, we defined PeLSCs for parametric properties by introducing assignment and condition structures into LSCs. With these structures, PeLSC can be interpreted over parametrized event traces. The language can than intuitively express requirement of data (e.g., values of time or other variables) carried by events. We developed translation from PeLSCs into HL for monitoring. We prove that the complexity of the word problem of PeLSCs is linear if propositions in the condition structures only express comparisons of terms.
There are several interesting topics for future work. Firstly, in this paper, we only concerned comparisons of terms in the condition structures. It is interesting to find out whether or not the PeLSC is still feasible for monitoring if the expressiveness of conditions is extended by, e.g., introducing quantifiers ∀ and ∃. Secondly, since the sizes of resulting formulae are often large, translating PeLSC into HL formulae is not an efficient way for monitoring. Therefore, we are currently developing a more efficient implementation, which can check PeLSC specifications directly. Last but not least, the synthesis problem of PeLSC based monitors is left open in this paper. As PeLSCs have features of the first order logic, the existing LSC synthesising techniques cannot handle this problem.