Impartiality and Anticipation for Monitoring of Visibly Context-Free Properties - Runtime Verification - page 183

Impartiality and Anticipation for Monitoring
of Visibly Context-Free Properties
Normann Decker, Martin Leucker, and Daniel Thoma
Institute for Software Engineering and Programming Languages
Universitat zu Lubeck, Germany
{ decker,leucker,thoma } @isp.uni-luebeck.de
Abstract. We study monitoring of visibly context-free properties. These
properties reflect the common concept of nesting which arises naturally
in software systems. They can be expressed e.g. in the temporal logic
CaRet which extends LTL by means of matching calls and returns. The
future fragment of CaRet enables us to give a direct unfolding-based
automaton construction, similar to LTL. We provide a four-valued, im-
partial semantics on finite words which is particularly suitable for mon-
itoring. This allows us to synthesize monitors in terms of deterministic
push-down Mealy machines. To go beyond impartiality, we develop a con-
struction for anticipatory monitors from visibly push-down ω -automata
by utilizing a decision procedure for emptiness.
1 Introduction
In Runtime Verification (RV) an actual execution of a system is checked with
respect to a given correctness property [1]. Therefore, typically a so-called mon-
itor is synthesized from the high-level specification of the correctness property,
which yields an assessment or a verdict , denoting to which extent the property
is satisfied by the current execution.
RV is a verification technique that is becoming more and more popular in
recent years but is also a key ingredient in new programming paradigms such as
monitor-oriented programming [2] or software architectures for reliable systems
such as runtime reflection [1].
In runtime verification, one always faces a finite execution of a potentially
infinite run of a system. Such an execution may be completed, and for exam-
ple, completely stored in a log file and subsequently checked with respect to
some property, or it may be checked on-line while it is continuously evolving.
Depending on the application, different notions of correctness assessments are
appropriate and monitors evaluating an execution and a property accordingly
are needed.
As explained in [3] and [4], a two-valued assessment yielding yes/true or
no/false seems appropriate when faced with completed executions as either a
property is satisfied or not.
When checking an execution on-line, at least three different assessments
( true / false / inconclusive ) are needed to adhere to the maxim of impartiality .