ISEP - DM - Engenharia de Sistemas Computacionais Críticos
Permanent URI for this collection
Browse
Browsing ISEP - DM - Engenharia de Sistemas Computacionais Críticos by Subject "Computation Tree Logic"
Now showing 1 - 1 of 1
Results Per Page
Sort Options
- Application of model checking in the formal verification of requirements for a speed control system in railwayPublication . COELHO, CRISTIANO MANUEL GARCÊS; Pinho, Luís Miguel Rosário da SilvaRailway 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.