Feu de bois

Les systèmes basés sur des règles semblent naturels pour la vérification de l'exécution (RV)/la surveillance des programmes. Du point de vue de la notation des spécifications, les systèmes basés sur des règles semblent tout à fait appropriés pour exprimer le type de propriétés que la communauté de vérification d'exécution écrit normalement. Les spécifications écrites dans un système de règles ont une saveur opérationnelle, qui peut être considérée comme un inconvénient ou un avantage, selon le point de vue. La saveur opérationnelle rend les spécifications plus longues que dans la logique temporelle déclarative ou les expressions régulières; cependant, ils sont naturels à écrire. Une fois l'idée de base maîtrisée, l'écriture de règles est simple, comme la programmation. Des spécifications plus déclaratives peuvent être plus difficiles à obtenir correctement. Cette observation est similaire à l'observation selon laquelle il peut être plus facile de formuler une propriété non triviale sous la forme d'une machine à états que sous la forme d'une formule de logique temporelle ou d'une expression régulière.

Les rovers et engins spatiaux du JPL produisent des flux de télémétrie lorsqu'ils fonctionnent. Un flux de télémétrie est essentiellement une séquence d'événements qui est stockée sur le terrain sous forme de journal dans une mémoire persistante. Les opérations de la mission doivent produire des vérifications automatisées de l'exactitude de ces journaux. LogFire peut être utilisé pour vérifier ces journaux. LogFire, par exemple, permet aux ingénieurs d'exploitation de s'assurer automatiquement qu'un mobile effectue les étapes correctes.

LogFire lit un fichier journal et le vérifie par rapport à une spécification formelle. La spécification peut être formulée dans un langage basé sur des règles. Le langage de spécification basé sur des règles est implémenté en tant qu'API dans le langage de programmation Scala. Il en résulte un langage de spécification très puissant puisque l'on peut mélanger règles et programmation traditionnelle.

La définition du langage basé sur des règles en tant qu'API dans Scala a l'apparence d'un DSL (Domain-Specific Language) en raison de la prise en charge par Scala de la définition de tels DSL (internes). Le moteur de règles, qui est basé sur l'algorithme RETE bien connu, a en outre été augmenté de la notion d'événements, qui sont instantanés contrairement aux faits de longue durée avec lesquels les moteurs de règles fonctionnent normalement. Enfin, une méthode d'indexation a optimisé le moteur pour gérer les événements qui transportent des données.

LogFire permet en outre d'encoder facilement des modèles de spécification pour générer des règles. Il est relativement simple de définir les modèles de spécification comme des fragments de logique temporelle et de lignes de temps - dont les instances sont traduites en règles. Une nuance intéressante est que ces modèles autorisent des événements paramétrés par les données. Des expériences ont été réalisées en comparant l'implémentation résultante avec six autres systèmes de vérification d'exécution et basés sur des règles.

La NASA cherche à concéder une licence gratuite pour ce logiciel et à le rendre disponible pour une utilisation générale pour des projets open source. Veuillez contacter le Concierge des licences de la NASA à Cette adresse e-mail est protégée contre les robots spammeurs. Vous devez activer le JavaScript pour la voir., ou appelez-nous au 202-358-7432 pour lancer des discussions sur les licences.