Resumo Técnico: Verificação de Sistemas SRA Configuráveis

Declaração do Problema

Sistemas digitais modernos, particularmente em controle embarcado e Sistemas em Chip (por exemplo, SystemC), são frequentemente projetados como sistemas Assíncronos Restritos por Agendador (SRA). Estes consistem em coleções de processos assíncronos orquestrados por um agendador específico de domínio que executa processos em fases discretas e não preemptivas. Embora a verificação formal de uma única instância SRA fixa seja estabelecida, a verificação de sistemas SRA configuráveis apresenta um desafio significativo.

Um SRA configurável descreve uma família ilimitada de sistemas possíveis definida por um conjunto de modelos de classe e restrições de configuração. Uma instância específica de sistema é gerada ao instanciar esses modelos com objetos concretos e interconexões que satisfazem as restrições. O objetivo da verificação é a verificação parametrizada: provar que uma propriedade global de segurança $\phi$ vale para toda instanciação legal do sistema configurável, em vez de verificar cada instância concreta individualmente. Isso é difícil devido às interações complexas entre processos, o agendador e a natureza ilimitada do espaço de configuração.

Metodologia

Os autores propõem uma abordagem de verificação dedutiva baseada em contratos, fundamentada na lógica de primeira ordem orientada a objetos. O framework utiliza o verificador de software Dafny como backend. A metodologia decompõe o problema global de verificação em obrigações locais através de três componentes principais:

1. Modelagem e Semântica

O sistema é modelado usando uma linguagem orientada a objetos onde:

• Classes representam tipos de processo, definidos como Máquinas de Estado Finito Estendidas (EFSMs) com transições guardadas por expressões booleanas e efeitos descritos como instruções imperativas.
• O Agendador é uma EFSM que coordena a execução de instâncias de classe através de fases discretas (locais).
• Configurações definem o conjunto concreto de objetos e suas conexões, restringidas por um conjunto de fórmulas lógicas $\Gamma$.

A semântica operacional distingue entre execução local (passos atômicos de instâncias individuais de processo) e execução global (ciclos orientados pelo agendador envolvendo auto-laços e transições de fase).

2. Estratégia de Verificação Composicional

Em vez de modelar explicitamente o agendador, a abordagem utiliza regras de prova composicionais para abstrair detalhes de agendamento. A estratégia central envolve:

• Contratos Locais: Geração automática de triplas de Hoare (pré-condições/pós-condições) para os métodos invocados pelo agendador (init, exec, tick). Esses contratos descrevem as mudanças de estado locais de uma única instância.
• Verificações de Consequência Global: Provar que um invariante global Inv é preservado pelas transições do agendador. Isso é alcançado por:
  • Inicialização: Mostrar que init estabelece Inv.
  • Preservação de Auto-laço: Provar que a execução de uma única instância preserva Inv sob uma condição local $g'_p$ (aproximando o guarda global), e usar indução para estender isso a intercalações arbitrárias de todas as instâncias.
  • Transições de Fase: Verificar que redefinições de estado e atualizações de temporizador (tick) preservam Inv.
  • Implicação de Segurança: Provar que Inv implica a propriedade alvo $\phi$ no final de cada ciclo de agendamento.

3. Automação e Otimização

• Geração Automática de Contratos: A cadeia de ferramentas executa simbolicamente os efeitos de transição para gerar as pré/pós-condições necessárias para os métodos exec, lidando com atribuições quantificadas e regras de prioridade.
• Aterramento de Quantificadores: Para configurações com tamanhos de conjuntos limitados (por exemplo, $|s| \le k$), o framework reescreve expressões quantificadas em conjunções/disjunções equivalentes sem quantificadores. Isso simplifica as condições de verificação para solvers SMT, preservando a equivalência lógica sob as restrições dadas.

Contribuições Principais

1. Framework Unificado para SRA Configuráveis: Uma formalização independente de domínio para verificar famílias ilimitadas de sistemas assíncronos restritos por agendador, indo além de trabalhos anteriores limitados a estudos de caso específicos ou topologias fixas.
2. Regras de Prova Composicionais: Um conjunto de regras dedutivas que abstraem o agendador, reduzindo provas de invariância global a contratos de método locais e verificações de consequência de primeira ordem.
3. Implementação Automática: Uma cadeia de ferramentas construída sobre o Dafny que gera automaticamente modelos, contratos e transformações de otimização (aterramento de quantificadores) a partir de descrições de alto nível de lógica de controle.
4. Avaliação Experimental Escalável: Validação em benchmarks de escala industrial (sistemas de controle ferroviário) envolvendo dezenas de milhares de linhas de código, demonstrando a capacidade de provar propriedades de segurança para todas as configurações válidas automaticamente.

Resultados Experimentais

O framework foi avaliado em benchmarks de sistemas industriais de controle ferroviário (Sistema de Proteção Ferroviária - RPS, Lógica de Controle de Sinais - SCL) e um Sistema de Controle de Robô Generalizado (RCS).

• Desempenho: A abordagem verificou com sucesso propriedades de segurança para sistemas com dezenas de milhares de linhas de código.
• Impacto da Otimização:
  • Baseado em Conjuntos vs. Baseado em Listas: A formalização baseada em teoria dos conjuntos superou as abordagens anteriores baseadas em listas, reduzindo o tempo de verificação e o consumo de recursos (RC) ao ocultar detalhes estruturais desnecessários.
  • Aterramento de Quantificadores: A aplicação de otimizações de aterramento reduziu significativamente o tempo de verificação e o uso de recursos, particularmente para propriedades complexas.
  • Nível de Método vs. Nível de Transição: A verificação de propriedades sobre o método exec (agregando transições) foi significativamente mais rápida do que a verificação sobre transições individuais, atribuída à melhor reutilização de informações do solver SMT.
• Estudos de Caso:
  • RPS: Verificou 25 propriedades de segurança (21 existentes, 4 novas) em bases de código de 10k–15k LoC.
  • SCL: Verificou a correção do aspecto do sinal em bases de código de ~6k LoC.
  • RCS: Verificou a evasão de obstáculos para um número ilimitado de sensores.

Significado e Alegações

O artigo alega fornecer uma solução prática e escalável para a verificação parametrizada de sistemas SRA configuráveis, uma classe de sistemas crítica para domínios de segurança crítica como ferrovias e controle embarcado.

• Automação: O framework reduz o esforço de anotação manual gerando automaticamente contratos e aproveitando o provador do Dafny, permitindo que engenheiros se concentrem na lógica do sistema em vez de detalhes de prova de baixo nível.
• Generalidade: Diferentemente de trabalhos anteriores restritos a conjuntos finitos de produtos ou topologias específicas, este framework lida com famílias ilimitadas com restrições de configuração flexíveis.
• Aplicabilidade Industrial: A aplicação bem-sucedida a sistemas reais de sinalização ferroviária demonstra que a verificação dedutiva pode escalar para complexidade industrial sem sacrificar a automação.

Os autores observam que, embora a decomposição e a geração de contratos sejam totalmente automatizadas, a descoberta de invariantes indutivos adequados para propriedades complexas pode ainda exigir intervenção manual, embora vejam a descoberta automática de invariantes como uma direção promissora para trabalhos futuros. O artigo não alega resolver a indecidibilidade geral da verificação parametrizada, mas sim fornece uma metodologia prática e eficaz para uma classe específica e importante de sistemas.