LogFire: Regelbasierte Laufzeitverifikation für zuverlässiges Systemmonitoring

Regelbasierte Systeme scheinen natürlich für Laufzeitverifikation (RV)/Programmmonitoring. Aus der Sicht einer Spezifikationsnotation erscheinen regelbasierte Systeme recht geeignet, um die Art von Eigenschaften auszudrücken, die die Laufzeitverifikationsgemeinschaft normalerweise schreibt. In einem Regelsystem geschriebene Spezifikationen haben einen operativen Charakter, der als Nachteil oder Vorteil gesehen werden kann, je nach Standpunkt. Der operative Charakter macht Spezifikationen länger als in deklarativer temporaler Logik oder regulären Ausdrücken; jedoch sind sie natürlich zu schreiben. Einmal die Kernidee beherrscht, ist das Schreiben von Regeln unkompliziert, wie Programmieren. Deklarativere Spezifikationen können trickreicher sein, richtig zu formulieren. Diese Beobachtung ähnelt der, dass es einfacher sein kann, eine nicht-triviale Eigenschaft als Zustandsmaschine zu formulieren als als temporallogische Formel oder regulärer Ausdruck.

JPLs Rover und Raumfahrzeuge produzieren Telemetriestreams während des Betriebs. Ein Telemetriestream ist im Wesentlichen eine Sequenz von Ereignissen, die am Boden als Log in persistentem Speicher gespeichert wird. Missionsoperationen müssen automatisierte Prüfungen erzeugen, dass diese Logs korrekt sind. LogFire kann zur Prüfung dieser Logs verwendet werden. LogFire ermöglicht beispielsweise Operationsingenieuren, automatisch sicherzustellen, dass ein Rover die korrekten Schritte ausführt.

LogFire liest eine Logdatei ein und prüft sie gegen eine formale Spezifikation. Die Spezifikation kann in einer regelbasierten Sprache formuliert werden. Die regelbasierte Spezifikationssprache ist als API in der Programmiersprache Scala implementiert. Dies resultiert in einer sehr mächtigen Spezifikationssprache, da man Regeln und traditionelle Programmierung mischen kann.

Die Definition der regelbasierten Sprache als API in Scala hat das Aussehen einer DSL (Domain-Specific Language) aufgrund von Scalas Unterstützung für die Definition solcher (interner) DSLs. Die Regel-Engine, die auf dem bekannten RETE-Algorithmus basiert, wurde zusätzlich mit dem Begriff von Ereignissen erweitert, die instantan sind im Gegensatz zu langlebigen Fakten, mit denen Regel-Engines normalerweise arbeiten. Schließlich hat eine Indizierungsmethode die Engine optimiert, um Ereignisse zu behandeln, die Daten tragen.

LogFire ermöglicht außerdem, Spezifikationsmuster einfach zu kodieren, um Regeln zu generieren. Es ist relativ unkompliziert, Spezifikationsmuster als Fragmente temporaler Logik und Zeitlinien zu definieren – Instanzen davon werden in Regeln übersetzt. Eine interessante Nuance ist, dass diese Vorlagen datenparametrisierte Ereignisse erlauben. Experimente wurden durchgeführt, die die resultierende Implementierung mit sechs anderen Laufzeitverifikations- und regelbasierten Systemen verglichen.

Die NASA strebt an, diese Software frei zu lizenzieren und für Open-Source-Projekte allgemein verfügbar zu machen. Bitte kontaktieren Sie die NASA Licensing Concierge unter dieser E-Mail-Adresse (JavaScript erforderlich) oder rufen Sie uns an unter 202-358-7432, um Lizenzgespräche zu initiieren.