LogFire: Regel-gebaseerde Runtime Verificatie Voor Betrouwbare Systeemmonitoring

Regel-gebaseerde systemen lijken natuurlijk voor runtime verificatie (RV)/programma monitoring. Van een specificatienotatie oogpunt, lijken regel-gebaseerde systemen geschikt voor het uitdrukken van de eigenschappen die de runtime verificatie gemeenschap normaal schrijft. Specificaties geschreven in een regelsysteem hebben een operationele smaak, wat gezien kan worden als een nadeel of een voordeel, afhankelijk van het standpunt. De operationele smaak maakt specificaties langer dan in declaratieve temporele logica of reguliere expressies; echter, ze zijn natuurlijk om te schrijven. Eenmaal het kernidee onder de knie is, is het schrijven van regels eenvoudig, als programmeren. Meer declaratieve specificaties kunnen lastiger zijn om goed te krijgen. Deze observatie is vergelijkbaar met de observatie dat het makkelijker kan zijn om een niet-triviale eigenschap te formuleren als een toestandsmachine dan als een temporele logica formule of een reguliere expressie.

JPL's rovers en ruimtevaartuigen produceren telemetriestromen tijdens het opereren. Een telemetriestroom is essentieel een reeks gebeurtenissen die op de grond opgeslagen wordt als een log in persistent geheugen. Missie-operaties moeten geautomatiseerde controles produceren dat deze logs correct zijn. LogFire kan gebruikt worden voor het controleren van deze logs. LogFire stelt bijvoorbeeld operatie-ingenieurs in staat om automatisch te verzekeren dat een rover de correcte stappen uitvoert.

LogFire leest een logbestand in en controleert het tegen een formele specificatie. De specificatie kan geformuleerd worden in een regel-gebaseerde taal. De regel-gebaseerde specificatietaal is geïmplementeerd als een API in de Scala programmeertaal. Dit resulteert in een zeer krachtige specificatietaal aangezien men regels en traditioneel programmeren kan mengen.

De definitie van de regel-gebaseerde taal als een API in Scala heeft de uitstraling van een DSL (Domain-Specific Language) door Scala's ondersteuning voor definitie van zulke (interne) DSL's. De regelengine, die gebaseerd is op het bekende RETE algoritme, is bovendien uitgebreid met de notie van gebeurtenissen, die instantane zijn in tegenstelling tot langlevende feiten waarmee regelengines normaal werken. Ten slotte heeft een indexeringsmethode de engine geoptimaliseerd om gebeurtenissen die data dragen te hanteren.

LogFire stelt bovendien specificatiepatronen in staat om eenvoudig gecodeerd te worden om regels te genereren. Het is relatief eenvoudig om specificatiepatronen te definiëren als fragmenten van temporele logica en tijdlijnen — instanties waarvan vertaald worden naar regels. Een interessante nuance is dat deze sjablonen data-geparametriseerde gebeurtenissen toestaan. Experimenten zijn uitgevoerd die de resulterende implementatie vergelijken met zes andere runtime verificatie en regel-gebaseerde systemen.

NASA streeft ernaar deze software vrij te licentiëren en beschikbaar te maken voor algemeen gebruik voor open source projecten. Neem contact op met NASA's Licensing Concierge via dit e-mailadres (beschermd tegen spambots, JavaScript vereist), of bel ons op 202-358-7432 om licentiegesprekken te initiëren.