Rule-based runtime verification revisited

Runtime verification (RV) consists in part of checking execution traces against user-provided formalized specifications. Throughout the last decade many new 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 relevant 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 rule-based system, named LogFire, for runtime verification, founded on the Rete algorithm, as an internal DSL in the Scala programming language (in essence a library). Using Scala’s support for defining DSLs allows to write rules elegantly as part of Scala programs. This combination appears attractive from a practical point of view. Our contribution is part conceptual in arguing that such rule-based frameworks originating from AI are suited for RV. Our contribution is technical by implementing an internal rule DSL in Scala; by illustrating how specification patterns can easily be encoded that generate rules, and by adapting and optimizing the Rete algorithm for RV purposes. An experimental evaluation is performed comparing to six other trace analysis systems. LogFire is currently being used to process telemetry from the Mars Curiosity rover at NASA’s Jet Propulsion Laboratory.