Houtvuur

Regelgebaseerde systemen lijken natuurlijk voor runtime-verificatie (RV)/programmabewaking. Vanuit het oogpunt van specificatienotatie lijken op regels gebaseerde systemen heel geschikt om het soort eigenschappen uit te drukken dat de runtime-verificatiegemeenschap normaal schrijft. Specificaties geschreven in een regelsysteem hebben een operationele smaak, die kan worden gezien als een nadeel of een voordeel, afhankelijk van het gezichtspunt. De operationele smaak maakt specificaties langer dan in declaratieve temporele logica of reguliere expressies; ze zijn echter natuurlijk om te schrijven. Als het kernidee eenmaal onder de knie is, is het schrijven van regels eenvoudig, net als programmeren. Meer declaratieve specificaties kunnen lastiger zijn om goed te krijgen. Deze observatie is vergelijkbaar met de observatie dat het misschien gemakkelijker is om een ​​niet-triviale eigenschap te formuleren als een toestandsmachine dan als een temporele logische formule of een reguliere expressie.

JPL's rovers en ruimtevaartuigen produceren telemetriestromen tijdens het gebruik. Een telemetriestroom is in wezen een reeks gebeurtenissen die op de grond wordt opgeslagen als een logboek in een permanent geheugen. Missie-operaties moeten geautomatiseerde controles produceren dat deze logboeken correct zijn. LogFire kan worden gebruikt om deze logs te controleren. Met LogFire kunnen operations engineers bijvoorbeeld automatisch zorgen dat een rover de juiste stappen uitvoert.

LogFire leest een logbestand in en toetst het aan een formele specificatie. De specificatie kan worden geformuleerd in een op regels gebaseerde taal. De op regels gebaseerde specificatietaal is geïmplementeerd als een API in de programmeertaal Scala. Dit resulteert in een zeer krachtige specificatietaal omdat men regels en traditionele programmering kan combineren.

De definitie van de op regels gebaseerde taal als een API in Scala heeft het uiterlijk van een DSL (Domain-Specific Language) vanwege Scala's ondersteuning voor het definiëren van dergelijke (interne) DSL's. De rule engine, die gebaseerd is op het bekende RETE-algoritme, is bovendien uitgebreid met de notie van gebeurtenissen, die ogenblikkelijk zijn in tegenstelling tot langlevende feiten waarmee rule engines normaal werken. Ten slotte heeft een indexeringsmethode de engine geoptimaliseerd voor het verwerken van gebeurtenissen die gegevens bevatten.

Met LogFire kunnen bovendien specificatiepatronen eenvoudig worden gecodeerd om regels te genereren. Het is relatief eenvoudig om specificatiepatronen te definiëren als fragmenten van temporele logica en tijdlijnen - waarvan voorbeelden worden vertaald naar regels. Een interessante nuance is dat deze sjablonen data-geparametriseerde gebeurtenissen mogelijk maken. Er zijn experimenten uitgevoerd om de resulterende implementatie te vergelijken met zes andere runtime-verificatie en op regels gebaseerde systemen.

NASA streeft ernaar deze software vrijelijk in licentie te geven en beschikbaar te stellen voor algemeen gebruik voor open source-projecten. Neem contact op met NASA's Licensing Concierge via Dit e-mailadres wordt beveiligd tegen spambots. U heeft Javascript nodig om het te kunnen zien., of bel ons op 202-358-7432 om licentiebesprekingen te starten.