Rule-based systems seem natural for runtime verification (RV)/program monitoring. From a specification notation point of view, rule-based systems appear quite suitable for expressing the kind of properties the runtime verification community normally writes. Specifications written in a rule system have an operational flavor, which can be seen as a disadvantage or an advantage, depending on the viewpoint. The operational flavor makes specifications longer than in declarative temporal logic or regular expressions; however, they are natural to write. Once the core idea is mastered, writing rules is straightforward, like programming. More declarative specifications can be trickier to get right. This observation is similar to the observation that it may be easier to formulate a nontrivial property as a state machine than as a temporal logic formula or a regular expression.
JPL’s rovers and spacecraft produce telemetry streams when operating. A telemetry stream is essentially a sequence of events that is stored on the ground as a log in persistent memory. Mission operations need to produce automated checks that these logs are correct. LogFire can be used for checking these logs. LogFire, for example, allows operations engineers to automatically ensure that a rover performs the correct steps.
LogFire reads in a log file and checks it against a formal specification. The specification can be formulated in a rule-based language. The rule-based specification language is implemented as an API in the Scala programming language. This results in a very powerful specification language since one can mix rules and traditional programming.
The definition of the rule-based language as an API in Scala has the appearance of a DSL (Domain-Specific Language) due to Scala’s support for definition of such (internal) DSLs. The rule engine, which is based on the well known RETE algorithm, has in addition been augmented with the notion of events, which are instantaneous in contrast to long-living facts with which rule engines normally work. Finally, an indexing method has optimized the engine to handle events that carry data.
LogFire furthermore allows specification patterns to be easily encoded to generate rules. It is relatively straightforward to define specification patterns as fragments of temporal logic and time lines — instances of which are translated to rules. An interesting nuance is that these templates allow data-parameterized events. Experiments have been performed comparing the resulting implementation with six other runtime verification and rule-based systems.