Mechanised Local Deadlock Analysis based on Timed Behavioural
Patterns and Responsiveness
Sistemas de Controle, Simulink, Semântica, Métodos Formais,
CSP, tock-CSP, Deadlock, Redes Temporizadas, Padrões, Responsividade
Embora o Desenvolvimento Dirigido por Modelos (MDD do inglês model driven
development) auxilie a identificação de problemas no design nas fases
iniciais do desenvolvimento com o uso de ambientes de simulação como o
Matlab/Simulink, os guias mais recentes para a verificação neste contexto
(como a DO178C) sugerem o uso de verificação formal para estes sistemas.
Neste contexto, várias abordagens vem sendo propostas para realizar a
tradução de Simulink para uma notação formal. Entretanto, a maioria dessas
abordagens não é focada na verificação composicional para permitir
escalabilidade; ou não provê a rastreabilidade dos resultados da
verificação formal. Em trabalhos anteriores, desenvolvemos uma estratégia
que usa a notação Communicating Sequential Processes (𝐶𝑆𝑃) para verificar
modelos Simulink, mas ela era limitada a verificação de modelos usando a
ferramenta Failures-Divergence Refinement (𝐹𝐷𝑅); então modificamos a
estratégia para prover a análise de composicional de deadlock para redes de
process temporizadas, mais especificamente, aquelas obtidas a partir de
diagramas de bloco multi-taxa discretos do Simulink. A estratégia
modificada estende a teoria de análise composicional de deadlock de Roscoe
e Dathi. No entanto, a principal limitação da abordagem proposta é que ela
foi restrita a modelos com um grafo de comunicação acíclico. Este trabalho
estende esta última estratégia em duas direções: (1) lidamos com modelos
cíclicos, o que ocorre naturalmente em modelos Simulink com realimentação
(feedback), entre outros tipos de ciclos; e (2) concebemos uma abordagem de
verificação para a integração de sistemas, estendendo a noção de plug-ins
responsivos de Roscoe, Reed e Sinclair. Uma vez que não existe uma solução
geral para analisar modelos cíclicos de forma composicional, exploramos o
uso de padrões comportamentais que permitem que a verificação seja
realizada de forma composicional. Representamos redes de processo em
tock-𝐶𝑆𝑃, um dialeto de 𝐶𝑆𝑃 que permite modelar aspectos de tempo usando o
evento especial tock. A abordagem de verificação é codificada como um novo
pacote em 𝐶𝑆𝑃-𝑃𝑟𝑜𝑣𝑒𝑟, um provador de teoremas para 𝐶𝑆𝑃 que é codificado
em 𝐼𝑠𝑎𝑏𝑒𝑙𝑙��/𝐻𝑂𝐿. Para ilustrar a abordagem geral e, particularmente, como
ela pode escalar, consideramos, de forma crescente, diferentes níveis de
complexidade um exemplo de sistema de atuação para o controle longitudinal
de uma aeronave, incluindo um Sistema de Controle de Arfagem e um Sistema
de Controle de Estol. Mostramos que os exemplos são instâncias dos padrões
de comportamento temporizado cliente/servidor e assíncrono dinâmico. Esses
padrões e todas as etapas de verificação são formalizadas
usando 𝐶𝑆𝑃-𝑃𝑟𝑜𝑣𝑒𝑟. A corretude é baseada em uma conexão de Galois ligando a
semântica traces da especificação tock-𝐶𝑆𝑃 gerada e as trajetórias de
simulação resultantes de uma codificação em 𝐼𝑠𝑎𝑏𝑒𝑙𝑙𝑒/𝐻𝑂𝐿 da teoria de
semântica operacional para Simulink de Bouissou e Chapoutot.