共 11 条
- [11] SNOOK C, HOANG T S, DGHYAM D, Et al., Behaviour-driven formal model development, Formal Methods and Software Engineering, pp. 21-36, (2018)
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
来源：
关键词：
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
相关论文