Banca de DEFESA: PAULO ENEAS ROLIM BEZERRA

Uma banca de DEFESA de MESTRADO foi cadastrada pelo programa.
DISCENTE : PAULO ENEAS ROLIM BEZERRA
DATA : 21/03/2023
HORA: 09:00
LOCAL: Remoto: meet.google.com/jqh-arqa-hxs
TÍTULO:

Verificação e Especificação CSP de um Sistema de Intertravamento Ferroviário Baseado 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. 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. Neste trabalho é apresentada 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. Além disso, o modelo proposto permite automatizar a verificação formal do sistema por verificação de modelos, 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:
Presidente - 1639701 - MARCEL VINICIUS MEDEIROS OLIVEIRA
Interno - 1221251 - MARTIN ALEJANDRO MUSICANTE
Externo à Instituição - AUGUSTO CEZAR ALVES SAMPAIO - UFPE