Formal Method for Behavior Verification and Data Validation of Station Interlocking System

被引：0
|
作者：
Wang K. [1 ,2 ]
Wang X. [1 ,2 ]
Cheng P. [1 ,2 ]
Liu N. [2 ,3 ]
Zhang C. [4 ]
机构：
[1] School of Information Science and Technology, Southwest Jiaotong University, Chengdu
[2] National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Southwest Jiaotong University, Chengdu
[3] Graduate School of Tangshan, Southwest Jiaotong University, Tangshan
[4] Beijing HollySys Co., Ltd., Beijing
来源：
Xinan Jiaotong Daxue Xuebao/Journal of Southwest Jiaotong University | 2021年 / 56卷 / 03期
关键词：
Data validation; Formal verification; Functional simulation; Station interlocking system; Testing; Theorem proving;
D O I：
10.3969/j.issn.0258-2724.20191182
中图分类号：
学科分类号：
摘要：
Station interlocking system is a typical safety-critical system driven by data, which needs to verify the system behavior and confirm the correctness of data in the development. After analyzing the design specifications of the interlocking system, the initial system model was built automatically by the UML (unified modeling language) diagram, with the system properties and event flows described by Event-B language on RODIN platform. Subsequently, the refinement policy was used for hierarchical modeling, and the proof obligations of each layer were proved by theorem and the properties of the system attributions were verified. Thus, a reliable universal function model was obtained. Using a real station yard, the axioms of the model were proved and the interlocking data were validated as well. According to the formal verification and data validation in a given scenario, the subtle defects generated in the analysis of the system requirements could be found and corrected. Finally, the functional simulation and acceptance testing confirmed the correctness of the general model and the interlock data. This method not only improves the accuracy and hierarchy of the model-based development, but also verifies the universal behavior state of the system. Combined with axiomatic verification, the validation of interlocking data is realized. The function scenario can be simulated and tested based on the model, which can further improve the reliability of the universal function prototype of the system. Copyright ©2021 JOURNAL OF SOUTHWEST JIAOTONG UNIVERSITY. All rights reserved.
引用
收藏
页码：587 / 593and610
相关论文
共 11 条
  • [1] WANG Keming, WANG Zheng, Modeling and verification of control system specification for railway level crossings based on formal method, Journal of Southwest Jiaotong University, 54, 3, pp. 573-578, (2019)
  • [2] Functional safety of electrical/electronic/programmable electronic safety-reared systems: IEC 61508, (2005)
  • [3] KHAN U, AHMAD J, SAEED T, Et al., On the real time modeling of interlocking system of passenger lines of Rawalpindi Cantt train station, Complex Adaptive Systems Modeling, 4, 1, pp. 1-33, (2016)
  • [4] VU L H, HAXTHAUSEN A E, PELESKA J., Formal modelling and verification of interlocking systems featuring sequential release, Science of Computer Programming, 133, pp. 91-115, (2017)
  • [5] BONACCHI A, FANTECHI A, BACHERINI S, Et al., Validation process for railway interlocking systems, Science of Computer Programming, 128, pp. 2-21, (2016)
  • [6] HANSEN D, SCHNEIDER D, LEUSCHEL M., Using B and ProB for data validation projects, Inernational Conference on Abstract State Machines, pp. 167-182, (2016)
  • [7] ABRIAL J R., Train system, Modeling in Event-B, pp. 508-549, (2013)
  • [8] (2015)
  • [9] (2017)
  • [10] ZHANG Chuandong, WANG Keming, WANG Xia, Et al., Interlocking data
12