Please use this identifier to cite or link to this item: https://repositorio.ufrn.br/handle/123456789/52600
Title: Especificação e verificação CSP de um sistema de intertravamento ferroviário baseado em relé
Other Titles: CSP specification and verification of a relay-based rail interlocking system
Authors: Bezerra, Paulo Eneas Rolim
Advisor: Oliveira, Marcel Vinicius Medeiros
Keywords: Computação;Formal methods;CSP;Railway interlocking systems
Issue Date: 21-Mar-2023
Publisher: Universidade Federal do Rio Grande do Norte
Citation: BEZERRA, Paulo Eneas Rolim. CSP specification and verification of a relay-based rail interlocking system. Orientador: Marcel Vinícius Medeiros Oliveira. 2023. 125f. Dissertação (Mestrado em Sistemas e Computação) - Centro de Ciências Exatas e da Terra, Universidade Federal do Rio Grande do Norte, Natal, 2023.
Portuguese Abstract: 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
Abstract: Railway Interlocking Systems (RIS) have long been implemented as relay-based systems. However, checking these systems for safety is usually done manually from an analysis of electrical circuit diagrams, which cannot be considered trustful. In the literature, formal verification approaches are used in order to analyse such systems. However, this type of verification tends to consume a lot of computational resources, which hinders the use of these verifications for industrial systems Although formal proof of the behaviour of these systems is effective in order to improve safety, in the existing literature, the works generally focus on modelling the system state transitions, ignoring the components independent concurrent behaviours. As a consequence, it is not possible to verify the existence of concurrency problems. Differently from other approaches, the methodology proposed in this work allows the specification of transient states. As a result, it is possible to perform a stronger verification, including an investigation about the existence of state succession cycles (i.e. ringbell effect), which are dangerous in such systems. A formal analysis of the system has the potential to guarantee its safety. This work presents a proposal for a formal specification model of the states of the electrical components of relay-based RIS using a process algebraic language, CSP. This model allows for the verification of such systems by analyzing the behavior of each component, allowing for the analysis of ringbell effect, short-circuits, deadlocks, divergences, and components that cannot be activated at same time. Based on the preconditions of the component states, the analysis and logical verification of the system become simpler. Furthermore, the proposed model facilitates the automation of the formal verification of the system by using model-checking, while focusing on the concurrency aspects of such systems and supporting the analysis of new safety conditions not previously considered.
URI: https://repositorio.ufrn.br/handle/123456789/52600
Appears in Collections:PPGSC - Mestrado em Sistemas e Computação

Files in This Item:
File SizeFormat 
EspecificacaoverificacaoCSP_Bezerra_2023.pdf3,9 MBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.