Lareira

Sistemas baseados em regras parecem naturais para verificação de tempo de execução (RV)/monitoramento de programas. Do ponto de vista da notação de especificação, os sistemas baseados em regras parecem bastante adequados para expressar o tipo de propriedades que a comunidade de verificação de tempo de execução normalmente escreve. As especificações escritas em um sistema de regras têm um sabor operacional, que pode ser visto como uma desvantagem ou vantagem, dependendo do ponto de vista. O sabor operacional torna as especificações mais longas do que na lógica temporal declarativa ou nas expressões regulares; no entanto, eles são naturais para escrever. Uma vez que a ideia central é dominada, escrever regras é simples, como programar. Especificações mais declarativas podem ser mais difíceis de acertar. Essa observação é semelhante à observação de que pode ser mais fácil formular uma propriedade não trivial como uma máquina de estados do que como uma fórmula lógica temporal ou uma expressão regular.

Os rovers e naves espaciais do JPL produzem fluxos de telemetria durante a operação. Um fluxo de telemetria é essencialmente uma sequência de eventos que é armazenada no solo como um log na memória persistente. As operações da missão precisam produzir verificações automatizadas de que esses logs estão corretos. O LogFire pode ser usado para verificar esses logs. O LogFire, por exemplo, permite que os engenheiros de operações garantam automaticamente que um rover execute as etapas corretas.

O LogFire lê um arquivo de log e o compara com uma especificação formal. A especificação pode ser formulada em uma linguagem baseada em regras. A linguagem de especificação baseada em regras é implementada como uma API na linguagem de programação Scala. Isso resulta em uma linguagem de especificação muito poderosa, pois pode-se misturar regras e programação tradicional.

A definição da linguagem baseada em regras como uma API em Scala tem a aparência de uma DSL (Domain-Specific Language) devido ao suporte do Scala para definição de tais DSLs (internas). O mecanismo de regras, que é baseado no conhecido algoritmo RETE, também foi ampliado com a noção de eventos, que são instantâneos em contraste com fatos duradouros com os quais os mecanismos de regras normalmente funcionam. Finalmente, um método de indexação otimizou o mecanismo para lidar com eventos que transportam dados.

Além disso, o LogFire permite que padrões de especificação sejam facilmente codificados para gerar regras. É relativamente simples definir padrões de especificação como fragmentos de lógica temporal e linhas de tempo – instâncias das quais são traduzidas em regras. Uma nuance interessante é que esses modelos permitem eventos parametrizados por dados. Experimentos foram realizados comparando a implementação resultante com seis outros sistemas de verificação em tempo de execução e baseados em regras.

A NASA procura licenciar livremente este software e disponibilizá-lo para uso geral em projetos de código aberto. Entre em contato com o Concierge de Licenciamento da NASA em Este endereço de e-mail está protegido contra spambots. Você precisa habilitar o JavaScript para visualizá-lo. ou ligue para 202-358-7432 para iniciar discussões sobre licenciamento.