LogFire: Verificación de tiempo de ejecución basada en reglas para monitoreo de sistemas fiable

Los sistemas basados en reglas parecen naturales para la verificación de tiempo de ejecución (RV)/monitoreo de programas. Desde un punto de vista de notación de especificación, los sistemas basados en reglas parecen bastante adecuados para expresar el tipo de propiedades que la comunidad de verificación de tiempo de ejecución normalmente escribe. Las especificaciones escritas en un sistema de reglas tienen un sabor operacional, que puede verse como una desventaja o una ventaja, dependiendo del punto de vista. El sabor operacional hace que las especificaciones sean más largas que en lógica temporal declarativa o expresiones regulares; sin embargo, son naturales de escribir. Una vez que se domina la idea central, escribir reglas es directo, como programar. Especificaciones más declarativas pueden ser más difíciles de acertar. Esta observación es similar a la observación de que puede ser más fácil formular una propiedad no trivial como una máquina de estados que como una fórmula de lógica temporal o una expresión regular.

Los rovers y naves espaciales de JPL producen flujos de telemetría cuando operan. Un flujo de telemetría es esencialmente una secuencia de eventos que se almacena en tierra como un registro en memoria persistente. Las operaciones de misión necesitan producir comprobaciones automatizadas de que estos registros son correctos. LogFire puede usarse para comprobar estos registros. LogFire, por ejemplo, permite a los ingenieros de operaciones asegurar automáticamente que un rover realiza los pasos correctos.

LogFire lee un archivo de registro y lo comprueba contra una especificación formal. La especificación puede formularse en un lenguaje basado en reglas. El lenguaje de especificación basado en reglas se implementa como una API en el lenguaje de programación Scala. Esto resulta en un lenguaje de especificación muy poderoso ya que se pueden mezclar reglas y programación tradicional.

La definición del lenguaje basado en reglas como una API en Scala tiene la apariencia de un DSL (Lenguaje Específico de Dominio) debido al soporte de Scala para definición de tales DSLs internos. El motor de reglas, que se basa en el bien conocido algoritmo RETE, ha sido además aumentado con la noción de eventos, que son instantáneos en contraste con hechos de larga vida con los que los motores de reglas normalmente trabajan. Finalmente, un método de indexación ha optimizado el motor para manejar eventos que llevan datos.

LogFire además permite que patrones de especificación se codifiquen fácilmente para generar reglas. Es relativamente directo definir patrones de especificación como fragmentos de lógica temporal y líneas de tiempo — instancias de las cuales se traducen a reglas. Un matiz interesante es que estas plantillas permiten eventos parametrizados por datos. Se han realizado experimentos comparando la implementación resultante con otros seis sistemas de verificación de tiempo de ejecución y basados en reglas.

NASA busca licenciar libremente este software y hacerlo disponible para uso general en proyectos de código abierto. Por favor contacte al Concierge de Licencias de NASA en Esta dirección de correo electrónico está protegida contra spambots. Necesita tener JavaScript habilitado para verla., o llámenos al 202-358-7432 para iniciar discusiones de licenciamiento.