Pós-Graduação em Ciência da Computação – UFPE
Defesa de Tese de Doutorado Nº 608
Aluno: Joabe Bezerra de Jesus Júnior
Orientador: Augusto Cezar Alves Sampaio
Título: Mechanised Local Deadlock Analysis based on Timed Behavioural Patterns and Responsiveness
Data: 28/08/2023
Hora/Local: 9h – Virtual – Interessados em assistir entrar em contato com o aluno
Banca Examinadora:
Prof. Juliano Manabu Iyoda(UFPE / Centro de Informática)
Prof. Eduardo Antonio Guimarães Tavares(UFPE / Centro de Informática)
Prof. Marcio Lopes Cornélio (UFPE / Centro de Informática)
Prof. Valdivino Alexandre de Santiago Junior (INPE / Coordenação de Pesquisa
Aplicada e Desenvolvimento Tecnológico)
Prof. Marcel Vinicius Medeiros Oliveira (UFRN / Departamento de Informática e Matemática Aplicada)
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.
Palavras-chave: Sistemas de Controle, Simulink, Semântica, Métodos Formais, CSP, tock-CSP, Deadlock, Redes Temporizadas, Padrões, Responsividade
Comentários desativados