Information Technology Reference
In-Depth Information
A Scala DSL for Rete-Based
Runtime Verification
Klaus Havelund
Jet Propulsion Laboratory
California Institute of Technology, California, USA
Abstract.
Runtime verification (RV) consists in part of checking ex-
ecution traces against formalized specifications. Several systems have
emerged, most of which support specification notations based on state
machines, regular expressions, temporal logic, or grammars. The field of
Artificial Intelligence (AI) has for an even longer period of time studied
rule-based production systems, which at a closer look appear to be rele-
vant for RV, although seemingly focused on slightly different application
domains, such as for example business processes and expert systems. The
core algorithm in many of these systems is the Rete algorithm. We have
implemented a Rete-based runtime verification system, named LogFire
(originally intended for oine log analysis but also applicable to online
analysis), as an internal DSL in the Scala programming language, using
Scala's support for defining DSLs. This combination appears attractive
from a practical point of view. Our contribution is in part conceptual
in arguing that such rule-based frameworks originating from AI may be
suited for RV.
1 Introduction
Runtime Verification (RV) consists of monitoring the behavior of a system, either
online as it executes, or oine after its execution, for example by analyzing log
files. Although this task seems easier than verification of all possible executions,
this task is challenging. From an
algorithmic
point of view the challenge consists
of eciently processing events that carry data. When a monitor receives an event,
it has to eciently locate what part of the monitor is relevant to activate, as a
function of the data carried by the event. This is called the
matching problem
.
From an
expressiveness
point of view, a logic should be as expressive as possible.
From a
elegance
point of view a logic should be easy to use and succinct for simple
properties. The problem has been addressed in several monitoring systems within
the last years. Most of these systems implement specification languages which
are based on state machines, regular expressions, temporal logic, or grammars.
The most ecient of these, for example [11], however, tend to have limited
expressiveness as discussed in [3].
The work described in this publication was carried out at Jet Propulsion Laboratory,
California Institute of Technology, under a contract with the National Aeronautics
and Space Administration.
