LogFire: Verificação de Tempo de Execução Baseada em Regras para Monitoramento Confiável de Sistemas

Sistemas baseados em regras parecem naturais para verificação de tempo de execução (RV)/monitoramento de programas. Do ponto de vista de notação de especificação, 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. Especificações escritas em um sistema de regras têm um sabor operacional, que pode ser visto como desvantagem ou vantagem, dependendo do ponto de vista. O sabor operacional torna as especificações mais longas do que em lógica temporal declarativa ou expressões regulares; no entanto, são naturais de escrever. Uma vez que a ideia central é dominada, escrever regras é direto, como programar. Especificações mais declarativas podem ser mais complicadas de acertar. Esta observação é similar à 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 de lógica temporal ou uma expressão regular.

Rovers e naves espaciais da JPL produzem streams de telemetria quando operam. Um stream de telemetria é essencialmente uma sequência de eventos que é armazenada no solo como um log em memória persistente. Operações de missão precisam produzir verificações automatizadas de que esses logs estão corretos. LogFire pode ser usado para verificar esses logs. LogFire, por exemplo, permite que engenheiros de operações garantam automaticamente que um rover execute os passos corretos.

LogFire lê um arquivo de log e o verifica contra 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 motor de regras, que é baseado no bem conhecido algoritmo RETE, foi adicionalmente aumentado com a noção de eventos, que são instantâneos em contraste com fatos de longa duração com os quais motores de regras normalmente trabalham. Finalmente, um método de indexação otimizou o motor para lidar com eventos que carregam dados.

LogFire também permite que padrões de especificação sejam facilmente codificados para gerar regras. É relativamente direto definir padrões de especificação como fragmentos de lógica temporal e linhas do tempo — instâncias dos quais são traduzidas para regras. Um matiz interessante é que esses templates permitem eventos parametrizados por dados. Experimentos foram realizados comparando a implementação resultante com seis outros sistemas de verificação de tempo de execução e baseados em regras.

A NASA busca licenciar livremente este software e torná-lo disponível para uso geral em projetos de código aberto. Por favor, contate o Concierge de Licenciamento da NASA em Este endereço de e-mail está protegido contra spambots. Você precisa de JavaScript habilitado para visualizá-lo., ou ligue para 202-358-7432 para iniciar discussões de licenciamento.