Fuego de leña

Los sistemas basados ​​en reglas parecen naturales para la verificación en tiempo de ejecución (RV)/monitoreo de programas. Desde el punto de vista de la notación de especificaciones, los sistemas basados ​​en reglas parecen bastante adecuados para expresar el tipo de propiedades que normalmente escribe la comunidad de verificación en tiempo de ejecución. Las especificaciones escritas en un sistema de reglas tienen un sabor operativo, que puede verse como una desventaja o una ventaja, según el punto de vista. El sabor operacional hace que las especificaciones sean más largas que en la lógica temporal declarativa o las expresiones regulares; sin embargo, son naturales para escribir. Una vez que se domina la idea central, escribir reglas es sencillo, como programar. Las especificaciones más declarativas pueden ser más difíciles de hacer bien. 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 estado que como una fórmula lógica temporal o una expresión regular.

Los rovers y las naves espaciales del JPL producen flujos de telemetría cuando están en funcionamiento. Un flujo de telemetría es esencialmente una secuencia de eventos que se almacena en el suelo como un registro en la memoria persistente. Las operaciones de la misión deben producir verificaciones automáticas de que estos registros sean correctos. LogFire se puede utilizar para comprobar estos registros. LogFire, por ejemplo, permite a los ingenieros de operaciones asegurarse automáticamente de que un móvil realice los pasos correctos.

LogFire lee un archivo de registro y lo compara con una especificación formal. La especificación se puede formular 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 da como resultado un lenguaje de especificación muy potente, 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 del dominio) debido al soporte de Scala para la definición de dichos DSL (internos). El motor de reglas, que se basa en el conocido algoritmo RETE, también se ha mejorado con la noción de eventos, que son instantáneos en contraste con los hechos de larga duración con los que normalmente funcionan los motores de reglas. Finalmente, un método de indexación ha optimizado el motor para manejar eventos que transportan datos.

Además, LogFire permite que los patrones de especificación se codifiquen fácilmente para generar reglas. Es relativamente sencillo definir patrones de especificación como fragmentos de lógica temporal y líneas de tiempo, cuyas instancias se traducen en 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 basados ​​en reglas y verificación en tiempo de ejecución.

NASA busca licenciar libremente este software y hacerlo disponible para uso general para proyectos de código abierto. Comuníquese con el Conserje de licencias de la NASA en Esta dirección de correo electrónico está protegida contra spambots. Necesita habilitar JavaScript para verlo o llámenos al 202-358-7432 para iniciar conversaciones sobre licencias.