Publication
Application of model checking in the formal verification of requirements for a speed control system in railway
| datacite.subject.fos | Engenharia e Tecnologia | |
| datacite.subject.sdg | 04:Educação de Qualidade | |
| dc.contributor.advisor | Pinho, Luís Miguel Rosário da Silva | |
| dc.contributor.author | COELHO, CRISTIANO MANUEL GARCÊS | |
| dc.date.accessioned | 2025-09-03T14:47:46Z | |
| dc.date.available | 2025-09-03T14:47:46Z | |
| dc.date.issued | 2025-07-25 | |
| dc.description.abstract | Railway speed control systems are essential for the safety and efficiency of railway transportation systems, as they ensure compliance with regulations and prevent accidents. As the demand for rail transport grows, rigorous verification of these systems is becomes increasingly critical. In such projects, errors are sometimes only detected during the testing phase, leading to costs that could have been avoided if these errors were identified in the early stages of the project. This thesis focuses on the topic of the formal verification of speed control system, specifically using model checking, to ensure that these systems meet safety requirements as well as performance standards. As the basis for the work presented in this thesis, we will adopt the EBICAB 700 architecture, and for which a small, yet representative, set of safety, operational, or regulatory requirements will be rigorously specified using well-known temporal logic languages, and verified against the system models using the model checking tools NuSMV and UPPAAL. This thesis work aims at contributing to the effort of demonstrating the feasibility and benefits of applying formal verification to railway systems, not only in terms of safety assurance but also as a strategy for reducing late-stage development risks and increased costs. It highlights the value of incorporating formal methods into the requirements and design phases of critical system engineering. | eng |
| dc.description.abstract | Os sistemas de controlo de velocidade ferroviária são essenciais para a segurança e eficiência dos sistemas de transporte ferroviário, pois garantem o cumprimento das regulamentações e previnem acidentes. À medida que cresce a procura pelo transporte ferroviário, a verificação rigorosa destes sistemas torna-se cada vez mais crítica. Em projetos deste tipo, os erros são por vezes detetados apenas na fase de testes, o que leva a custos que poderiam ter sido evitados se esses erros tivessem sido identificados nas fases iniciais do projeto. Esta tese foca-se na verificação formal de sistemas de controlo de velocidade, recorrendo especificamente à técnica de model checking, para garantir que estes sistemas cumprem os requisitos de segurança, bem como os padrões de desempenho. Como base para o trabalho apresentado nesta tese, será adotada como exemplo a arquitetura EBICAB 700, para a qual será especificado um conjunto pequeno, mas representativo, de requisitos de segurança, operacionais ou regulamentares, utilizando linguagens de lógica temporal bem conhecidas, e verificados contra os modelos do sistema através das ferramentas de model checking NuSMV e UPPAAL. O trabalho desta tese pretende contribuir para o esforço de demonstrar a viabilidade e os benefícios da aplicação da verificação formal em sistemas ferroviários, não apenas em termos de garantia de segurança, mas também como uma estratégia para reduzir riscos de desenvolvimento em fases tardias e os custos acrescidos. Destaca-se o valor da incorporação de métodos formais nas fases de requisitos e conceção da engenharia de sistemas críticos. | por |
| dc.identifier.tid | 203995562 | |
| dc.identifier.uri | http://hdl.handle.net/10400.22/30359 | |
| dc.language.iso | eng | |
| dc.rights.uri | N/A | |
| dc.subject | Speed control systems | |
| dc.subject | Linear Temporal Logic | |
| dc.subject | Computation Tree Logic | |
| dc.subject | Model checking | |
| dc.subject | Sistemas de controlo de velocidade | |
| dc.subject | Lógica temporal linear | |
| dc.subject | Lógica árvore de computação | |
| dc.subject | Verificação de modelos | |
| dc.title | Application of model checking in the formal verification of requirements for a speed control system in railway | eng |
| dc.title.alternative | Aplicação da verificação de modelos na verificação formal de requisitos para um sistema de controlo de velocidade em ferrovias | por |
| dc.type | master thesis | |
| dspace.entity.type | Publication | |
| thesis.degree.name | Mestrado em Engenharia de Sistemas Computacionais Críticos |