Holzfeuer

Regelbasierte Systeme scheinen für Laufzeitverifizierung (RV)/Programmüberwachung selbstverständlich. Vom Standpunkt der Spezifikationsnotation aus scheinen regelbasierte Systeme ziemlich geeignet zu sein, um die Art von Eigenschaften auszudrücken, die die Gemeinschaft der Laufzeitüberprüfung normalerweise schreibt. In einem Regelsystem geschriebene Spezifikationen haben einen operationalen Charakter, der je nach Sichtweise als Nachteil oder Vorteil angesehen werden kann. Der operationale Flavor macht Spezifikationen länger als in deklarativer temporaler Logik oder regulären Ausdrücken; sie sind jedoch natürlich zu schreiben. Sobald die Kernidee gemeistert ist, ist das Schreiben von Regeln einfach, wie das Programmieren. Deklarativere Spezifikationen können schwieriger zu finden sein. Diese Beobachtung ähnelt der Beobachtung, dass es möglicherweise einfacher ist, eine nichttriviale Eigenschaft als Zustandsmaschine zu formulieren als als temporale Logikformel oder als regulären Ausdruck.

Die Rover und Raumfahrzeuge des JPL erzeugen im Betrieb Telemetrieströme. Ein Telemetriestrom ist im Wesentlichen eine Abfolge von Ereignissen, die am Boden als Protokoll in einem dauerhaften Speicher gespeichert werden. Der Missionsbetrieb muss automatisiert prüfen, ob diese Protokolle korrekt sind. LogFire kann zur Überprüfung dieser Protokolle verwendet werden. Mit LogFire können Betriebsingenieure beispielsweise automatisch sicherstellen, dass ein Rover die richtigen Schritte ausführt.

LogFire liest eine Protokolldatei 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 führt zu 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), da Scala die Definition solcher (interner) DSLs unterstützt. Die Regelmaschine, die auf dem bekannten RETE-Algorithmus basiert, wurde zusätzlich um den Begriff der Ereignisse erweitert, die im Gegensatz zu langlebigen Fakten, mit denen Regelmaschinen normalerweise arbeiten, augenblicklich sind. Schließlich hat eine Indizierungsmethode die Engine optimiert, um Ereignisse zu verarbeiten, die Daten enthalten.

LogFire ermöglicht darüber hinaus die einfache Kodierung von Spezifikationsmustern zur Generierung von Regeln. Es ist relativ einfach, Spezifikationsmuster als Fragmente zeitlicher Logik und Zeitlinien zu definieren, deren Instanzen in Regeln übersetzt werden. Eine interessante Nuance ist, dass diese Vorlagen datenparametrisierte Ereignisse zulassen. Es wurden Experimente durchgeführt, bei denen die resultierende Implementierung mit sechs anderen Laufzeitüberprüfungs- und regelbasierten Systemen verglichen wurde.

Die NASA versucht, diese Software frei zu lizenzieren und sie für die allgemeine Nutzung für Open-Source-Projekte verfügbar zu machen. Bitte wenden Sie sich an den Licensing Concierge der NASA unter Diese E-Mail-Adresse ist vor Spambots geschützt! JavaScript muss aktiviert werden, damit sie angezeigt werden kann. Oder rufen Sie uns unter 202-358-7432 an, um Diskussionen über die Lizenzierung einzuleiten.