Simplifying the Formal Verification of Safety Requirements in Zone Controllers Through Problem Frames and Constraint-Based Projection

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, they aim to reduce the state space of formal verification problems in zone controller, a sub-system of a typical CBTC. They 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 frame-based method decomposes the system according to sub-properties through functional decomposition, while the constraint-based projection method removes redundant variables. The authors' industrial case study demonstrates the feasibility through an evaluation, confirming that these two methods are effective in reducing the state spaces of complex verification problems in this application domain.

• Record URL:
  https://doi.org/10.1109/TITS.2018.2869633
• Availability:
  • Find a library where document is available. Order URL: http://worldcat.org/oclc/41297384
• Supplemental Notes:
  • Copyright © 2018, IEEE.
• Authors:
  • Yuan, Zhengheng
  • Chen, Xiaohong
  • Liu, Jing
  • Yu, Yijun
  • Sun, Haiying
  • Zhou, Tingliang
  • Jin, Zhi
• Publication Date: 2018-11

Language

• English

Media Info

• Media Type: Digital/other
• Features: Figures; References; Tables;
• Pagination: pp 3517-3528
• Serial:
  • IEEE Transactions on Intelligent Transportation Systems
  • Volume: 19
  • Issue Number: 11
  • Publisher: Institute of Electrical and Electronics Engineers (IEEE)
  • ISSN: 1524-9050
  • Serial URL: http://ieeexplore.ieee.org/xpl/RecentIssue.jsp?punumber=6979

Subject/Index Terms

• TRT Terms: Algorithms; Automatic train control; Automatic train protection; Control devices; Railroad safety; Wireless communication systems
• Subject Areas: Data and Information Technology; Planning and Forecasting; Railroads; Safety and Human Factors; Vehicles and Equipment;

Filing Info

• Accession Number: 01690042
• Record Type: Publication
• Files: TLIB, TRIS
• Created Date: Dec 27 2018 3:43PM