Banca de QUALIFICAÇÃO: PAULO ENEAS ROLIM BEZERRA

Uma banca de QUALIFICAÇÃO de MESTRADO foi cadastrada pelo programa.
DISCENTE : PAULO ENEAS ROLIM BEZERRA
DATA : 19/12/2022
HORA: 09:00
LOCAL: Remoto: meet.google.com/sgn-hmiq-evk
TÍTULO:

Especificação CSP e Verificação de Sistemas de Intertravamento Ferroviário Baseados em Relés


PALAVRAS-CHAVES:

Model-checking, Métodos Formais, Communicating Sequential Process


PÁGINAS: 100
RESUMO:

Os Sistemas de Intertravamento Ferroviário (SIF) têm sido implementados há muito tempo como sistemas baseados em relés. No entanto, a verificação de segurança desses sistemas geralmente é feita manualmente a partir de uma análise de diagramas de circuitos elétricos, logo tal verificação não pode ser considerada confiável. Na literatura, abordagens com verificação formal são utilizadas para analisar tais sistemas. No entanto, esse tipo de verificação tende a consumir muitos recursos computacionais, o que dificulta o uso dessas verificações para sistemas industriais, o que torna a verificação de circuitos elétricos mais complexos não confiável. Embora a comprovação formal do comportamento desses sistemas seja eficaz para melhorar a segurança, na literatura existente, os trabalhos geralmente focam na modelagem das transições de estado do sistema, ignorando os comportamentos concorrentes dos componentes independentes. Como consequência, não é possível verificar a existência de problemas de concorrência. Diferentemente de outras abordagens, a metodologia proposta neste trabalho permite a especificação de estados transitórios. Como resultado, é possível realizar uma verificação mais forte, incluindo uma investigação sobre a existência de estados com ciclos sucessivos (ou seja, ringbell effect), que são perigosos em tais sistemas. Uma análise formal do sistema tem potencial para garantir sua segurança. Este trabalho apresenta uma proposta de modelo formal de especificação dos estados dos componentes elétricos de SIF baseados em relés utilizando uma linguagem baseada em processos, CSP. Este modelo permite a verificação de tais sistemas com base no comportamento de cada componente, o que permite a análise de certas propriedades como a existência de um estado com um ciclo infinito de sucessões (ou seja, ringbell effect), curtos-circuitos, deadlocks, divergências ou componentes que não podem estar ativados ao mesmo tempo, simplificando a análise e a verificação lógica do sistema com base nas pré-condições dos estados dos componentes. Além disso, o modelo proposto permite automatizar a verificação formal do sistema por model-checking, focando nos aspectos de concorrência de tais sistemas e fundamentando a análise de novas condições de segurança que não foram consideradas nas abordagens anteriores.


MEMBROS DA BANCA:
Interno - 1639701 - MARCEL VINICIUS MEDEIROS OLIVEIRA
Interno - 1221251 - MARTIN ALEJANDRO MUSICANTE
Interno - 1845280 - SERGIO QUEIROZ DE MEDEIROS
Notícia cadastrada em: 10/11/2022 23:07
SIGAA | Superintendência de Tecnologia da Informação - | | Copyright © 2006-2022 - UFRN - sigaa21-producao.info.ufrn.br.sigaa21-producao