Automated Repair of Requirements for Cyber-Physical Systems in Simulink Requirements Tables

Resumo Técnico: Reparo Automatizado de Requisitos para Sistemas Ciber-Físicos em Tabelas de Requisitos do Simulink

Declaração do Problema

O desenvolvimento de Sistemas Ciber-Físicos (CPSs) complexos envolve a evolução contínua e, frequentemente, independente da implementação do sistema e de seus requisitos. Essa independência cria um risco de desalinhamento, onde uma atualização do sistema (por exemplo, para mudanças de desempenho ou de hardware) torna o requisito original obsoleto ou incorreto. Embora o Reparo Automático de Programas (APR) aborde o desalinhamento modificando o sistema, ele assume que os requisitos estão corretos — uma premissa que frequentemente falha na prática, particularmente em domínios críticos de segurança onde os requisitos podem ser falhos, desatualizados ou inadequados.

As técnicas de APR existentes são inadequadas para reparar requisitos de CPS porque:

1. Desajuste de Domínio: O APR normalmente visa código imperativo ou modelos de alto nível, enquanto os requisitos de CPS são frequentemente fórmulas lógicas declarativas sobre sinais baseados em tempo e valores reais.
2. Granularidade: Os métodos existentes realizam frequentemente reparos de grão grosso (adição/remoção de blocos) ou são limitados a manipulações estruturais de expressões lógicas com suporte mínimo para raciocínio numérico sobre números reais.
3. Contexto: O APR depende de pistas contextuais (ex: código próximo) indisponíveis em requisitos declarativos isolados.

Consequentemente, há necessidade de uma estratégia complementar: o Reparo Automatizado de Requisitos, que modifica o requisito para corresponder ao comportamento evoluído do sistema, em vez de alterar o sistema em si.

Metodologia

Os autores propõem um framework que utiliza dados de execução do sistema (suítes de traços) para reparar requisitos desalinhados especificados na linguagem das Tabelas de Requisitos (RT) do MATLAB Simulink®.

1. Formalização do Problema de Reparo:

• Entrada: Uma suíte de traços $TS$ (uma coleção de traços de entrada/saída ao longo do tempo) e um requisito incorreto $r_0$.
• Saída: Um requisito reparado $r^*$ que é correto em relação a $TS$ (satisfeito por todos os traços) e otimizado de acordo com critérios de desejabilidade específicos.
• Semântica: O framework utiliza a semântica quantitativa das RTs, atribuindo um grau de satisfação a um requisito sobre um traço. Um requisito é correto se seu grau de satisfação for não negativo em todos os traços.

2. Framework de Otimização Multiobjetivo:
O processo de reparo é formulado como um problema de minimização multiobjetivo. O framework busca um conjunto de reparos Pareto-ótimos que equilibram a Correção com quatro Dimensões de Desejabilidade:

• Integridade Semântica ($d_{sem}$): Garante que o requisito reparado não seja trivial (não seja uma tautologia ou contradição) e seja consistente com propriedades do domínio (ex: compatibilidade de unidades).
• Similaridade Sintática ($d_{syn}$): Mede a distância estrutural (ex: distância de edição de árvore) entre o requisito original e o reparado para evitar complexidade desnecessária.
• Extensão de Satisfação ($d_{sat}$): Avalia a "magnitude" (o quão longe a fronteira do requisito está do comportamento observado) e a "amplitude" (com que frequência a precondição é violada, levando à verdade vacante) para garantir que o requisito seja informativo e não excessivamente amplo ou restritivo.

3. Algoritmo de Busca:
O framework emprega um loop de busca customizável (implementado usando algoritmos evolucionários na avaliação) consistindo em:

• Geração de Candidatos: Produz novos requisitos via operadores de mutação e crossover na gramática da RT.
• Avaliação: Computa os valores de fitness de correção e desejabilidade para cada candidato.
• Seleção: Utiliza ordenação não dominada para selecionar os melhores candidatos para a próxima geração.

Principais Contribuições

1. Definição do Problema: Uma definição formal do problema de reparo de requisitos para CPSs especificados em RT do Simulink, introduzindo uma noção de correção baseada em graus de satisfação quantitativos sobre suítes de traços.
2. Framework de Desejabilidade: Um novo framework multidimensional para avaliar a qualidade do reparo além da mera correção, incorporando integridade semântica, similaridade sintática e extensão de satisfação.
3. Framework Customizável: Um framework de reparo geral capaz de lidar com requisitos declarativos sobre sinais baseados em tempo e valores reais, uma capacidade que falta nas técnicas de APR existentes.
4. Avaliação Empírica: Uma avaliação extensa em seis estudos de caso do mundo real (incluindo modelos da Toyota, MathWorks e Lockheed Martin) cobrindo 12 requisitos.

Resultados

Os autores avaliaram sete variantes de seu framework através dos estudos de caso:

• Correção vs. Desejabilidade: O estudo encontrou um compromisso entre o número de reparos corretos encontrados e seus escores de desejabilidade. Uma estratégia de agregação usando objetivos separados (NoAgg) produziu uma maior quantidade de reparos corretos e semanticamente íntegros em comparação com uma estratégia de soma ponderada (WeiSum), embora esta última tenha gerado escores de desejabilidade ligeiramente melhores para os reparos encontrados.
• Verificação de Tautologia: O uso de uma verificação exata baseada em SMT para integridade semântica foi preferido em relação a uma abordagem baseada em amostragem devido à precisão, embora ambos tenham produzido quantidades semelhantes de reparos corretos.
• Parâmetros de Busca: Aumentar o número de descendentes (offspring) na busca evolucionária melhorou significamente o número de reparos de alta qualidade (corretos e semanticamente íntegros) encontrados, embora ao custo de maior tempo de execução.
• Utilidade: A análise de especialistas confirmou que o framework pode gerar reparos úteis e não triviais. Na maioria dos estudos de caso, um reparo útil foi encontrado dentro dos 3 principais candidatos classificados quando ordenados por similaridade sintática ou extensão de satisfação.
• Estudo de Ablação: Remover qualquer dimensão de desejabilidade (integridade semântica, similaridade sintática ou extensão de satisfação) degradou a qualidade geral dos reparos, confirmando que todas as três dimensões são necessárias para um reparo eficaz.

Significância e Alegações

O artigo afirma que seu framework aborda com sucesso a lacuna no reparo automatizado para requisitos declarativos de CPS. Ao mudar o foco de consertar o sistema para consertar o requisito, a abordagem fornece uma alternativa viável quando modificações no sistema são impraticáveis ou quando os requisitos são a fonte do desalinhamento.

Os autores enfatizam que seu trabalho não automatiza a decisão de quando reparar um requisito versus o sistema; em vez disso, assume que essa decisão foi tomada por engenheiros e fornece os meios técnicos para executar o reparo. O framework é significativo por sua capacidade de lidar com sinais baseados em tempo e valores reais e por sua integração de métricas de desejabilidade práticas (como evitar soluções triviais e manter a consistência do domínio) no processo de reparo. Os resultados demonstram que é possível derivar automaticamente requisitos que não são apenas matematicamente corretos em relação a traços de execução, mas também semanticamente significativos e sintaticamente próximos das especificações originais.