Banca de QUALIFICAÇÃO: PAULO ENEAS ROLIM BEZERRA

Uma banca de QUALIFICAÇÃO de MESTRADO foi cadastrada pelo programa.
STUDENT : PAULO ENEAS ROLIM BEZERRA
DATE: 19/12/2022
TIME: 09:00
LOCAL: Remoto: meet.google.com/sgn-hmiq-evk
TITLE:

CSP Specification and Verification of Relay-based Railway Interlocking Systems

KEY WORDS:

Model-Checking, Formal Methods, Communicating Sequential Process

PAGES: 100
BIG AREA: Ciências Exatas e da Terra
AREA: Ciência da Computação
SUBÁREA: Metodologia e Técnicas da Computação
SPECIALTY: Engenharia de Software
SUMMARY:

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 verification for industrial systems that makes the verification of more complex electrical circuits untrustworthy. 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-based language, CSP. This model enables the verification of such systems based on each component behaviour, which allows the analysis of properties like existence of a state with an infinity succession cycle (i.e. ringbell effect), short-circuits, deadlocks or divergences, by simplifying the analysis and logical verification of the system based on the preconditions of the component states. Furthermore, the proposed model allows the automation of the formal verification of the system by model-checking, focusing on the concurrency aspects of such systems and supporting the analysis of new safety conditions that were not considered on previous approaches.

COMMITTEE MEMBERS:
Interno - 1639701 - MARCEL VINICIUS MEDEIROS OLIVEIRA
Interno - 1221251 - MARTIN ALEJANDRO MUSICANTE
Interno - 1845280 - SERGIO QUEIROZ DE MEDEIROS