LogFire : vérification d'exécution basée sur règles pour surveillance système fiable

Systèmes basés sur règles pour vérification d'exécution

Les systèmes basés sur règles semblent naturels pour la vérification d'exécution (RV)/surveillance de programme. Du point de vue de la notation de spécification, ils apparaissent bien adaptés pour exprimer le type de propriétés que la communauté RV écrit normalement. Les spécifications écrites dans un système de règles ont une saveur opérationnelle, qui peut être vue comme désavantage ou avantage selon le point de vue. Cette saveur rend les spécifications plus longues qu'en logique temporelle déclarative ou expressions régulières ; cependant, elles sont naturelles à écrire. Une fois l'idée maîtresse comprise, écrire des règles est direct, comme programmer. Des spécifications plus déclaratives peuvent être plus délicates à bien formuler. Cette observation ressemble à celle qu'il peut être plus facile de formuler une propriété non-triviale comme machine à états que comme formule de logique temporelle ou expression régulière.

Application aux rovers et vaisseaux spatiaux JPL

Les rovers et vaisseaux spatiaux du JPL produisent des flux de télémétrie en fonctionnement. Un flux de télémétrie est essentiellement une séquence d'événements stockée au sol comme journal en mémoire persistante. Les opérations de mission doivent produire des vérifications automatisées que ces journaux sont corrects. LogFire peut être utilisé pour vérifier ces journaux. LogFire permet par exemple aux ingénieurs d'opérations de s'assurer automatiquement qu'un rover effectue les bonnes étapes.

LogFire lit un fichier journal et le vérifie contre une spécification formelle. La spécification peut être formulée dans un langage basé sur règles. Le langage de spécification basé sur règles est implémenté comme API dans le langage de programmation Scala. Cela résulte en un langage de spécification très puissant puisqu'on peut mélanger règles et programmation traditionnelle.

La définition du langage basé sur règles comme API en Scala a l'apparence d'un DSL (Domain-Specific Language) grâce au support de Scala pour la définition de tels DSLs internes. Le moteur de règles, basé sur l'algorithme RETE bien connu, a en plus été augmenté avec la notion d'événements, instantanés contrairement aux faits de longue durée avec lesquels les moteurs de règles travaillent normalement. Finalement, une méthode d'indexation a optimisé le moteur pour gérer les événements portant des données.

LogFire permet en outre d'encoder facilement des motifs de spécification pour générer des règles. Il est relativement direct de définir des motifs de spécification comme fragments de logique temporelle et lignes de temps — instances desquelles sont traduites en règles. Une nuance intéressante : ces patrons permettent des événements paramétrés par données. Des expériences ont comparé l'implémentation résultante avec six autres systèmes de vérification d'exécution et basés sur règles.

La NASA cherche à licencier gratuitement ce logiciel et le rendre disponible pour usage général pour projets open source. Contactez le concierge des licences NASA à l'adresse protégée, ou appelez au 202-358-7432 pour initier les discussions de licence.