Oliveira, Marcel Vinicius MedeirosBezerra, Paulo Eneas Rolim2023-06-022023-06-022023-03-21BEZERRA, 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.https://repositorio.ufrn.br/handle/123456789/52600Railway 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.Acesso AbertoComputaçãoFormal methodsCSPRailway interlocking systemsmasterThesisCNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO