Banca de DEFESA: JOABE BEZERRA DE JESUS JUNIOR

Uma banca de DEFESA de DOUTORADO foi cadastrada pelo programa.
DISCENTE: JOABE BEZERRA DE JESUS JUNIOR
DATA : 28/08/2023
HORA: 09:00
LOCAL: Virtual
TÍTULO:

Mechanised Local Deadlock Analysis based on Timed Behavioural 
Patterns and Responsiveness

PALAVRAS-CHAVES:

Sistemas de Controle, Simulink, Semântica, Métodos Formais, 
CSP, tock-CSP, Deadlock, Redes Temporizadas, Padrões, Responsividade

PÁGINAS: 154
RESUMO:

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.

MEMBROS DA BANCA:
Interno - 2743538 - EDUARDO ANTONIO GUIMARAES TAVARES
Presidente - 1670543 - JULIANO MANABU IYODA
Externo à Instituição - MARCEL VINICIUS MEDEIROS OLIVEIRA - UFRN
Interno - 1742011 - MARCIO LOPES CORNELIO
Externo à Instituição - VALDIVINO ALEXANDRE DE SANTIAGO JUNIOR - INPE