Loading...
Publication
Application of model checking in the formal verification of requirements for a speed control system in railway
| Name: | Description: | Size: | Format: | |
|---|---|---|---|---|
| 7.24 MB | Adobe PDF |
Authors
Advisor(s)
Abstract(s)
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.
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.
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.
Description
Keywords
Speed control systems Linear Temporal Logic Computation Tree Logic Model checking Sistemas de controlo de velocidade Lógica temporal linear Lógica árvore de computação Verificação de modelos
Pedagogical Context
Citation
Publisher
CC License
Without CC licence