Detalhes bibliográficos
| Ano de defesa: |
2023 |
| Autor(a) principal: |
Bezerra, Paulo Eneas Rolim |
| Orientador(a): |
Oliveira, Marcel Vinicius Medeiros |
| Banca de defesa: |
Não Informado pela instituição |
| Tipo de documento: |
Dissertação
|
| Tipo de acesso: |
Acesso aberto |
| Idioma: |
por |
| Instituição de defesa: |
Universidade Federal do Rio Grande do Norte
|
| Programa de Pós-Graduação: |
PROGRAMA DE PÓS-GRADUAÇÃO EM SISTEMAS E COMPUTAÇÃO
|
| Departamento: |
Não Informado pela instituição
|
| País: |
Brasil
|
| Palavras-chave em Português: |
|
| Área do conhecimento CNPq: |
|
| Link de acesso: |
https://repositorio.ufrn.br/handle/123456789/52600
|
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. 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 álgebra de 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 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 |
