Simplifying the Formal Verification of Safety Requirements in Zone Controllers Through Problem Frames and Constraint-Based Projection
| Autor: | Yijun Yu, Haiying Sun, Tingliang Zhou, Zhengheng Yuan, Jing Liu, Xiaohong Chen, Zhi Jin |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
050210 logistics & transportation
Mathematical optimization Computer science Mechanical Engineering 05 social sciences Frame (networking) 020207 software engineering 02 engineering and technology Functional decomposition Formal methods Computer Science Applications Control theory Control system 0502 economics and business Automotive Engineering 0202 electrical engineering electronic engineering information engineering State space Projection (set theory) Formal verification |
| Zdroj: | IEEE Transactions on Intelligent Transportation Systems. 19:3517-3528 |
| ISSN: | 1558-0016 1524-9050 |
| DOI: | 10.1109/tits.2018.2869633 |
| Popis: | Formal methods have been applied widely to verifying the safety requirements of Communication-Based Train Control (CBTC) systems, while the problem situations could be much simplified. In industrial practices of CBTC systems, however, huge complexity arises, which renders those methods nearly impossible to apply. In this paper, we aim to reduce the state space of formal verification problems in Zone Controller, a sub-system of a typical CBTC. We achieve the simplification goal by reducing the total number of device variables. To do this, two projection methods are proposed based on Problem Frames and constraints, respectively. The Problem Frames based method decomposes the system according to sub-properties through functional decomposition, whilst the constraints based projection method removes redundant variables. Our industrial case study demonstrates the feasibility though an evaluation, confirming that these two methods are effective in reducing the state spaces of complex verification problems in this application domain. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|