车站联锁系统行为验证与数据确认的形式化方法

车站联锁系统是一种典型的基于数据驱动的安全苛求系统，开发过程中需要对系统行为进行验证并需确认数据的正确性. 为此，通过分析联锁系统的设计规范，基于RODIN平台并使用Event-B语言，辅助使用UML （unified modeling language）图工具快速建立系统的初始模型，以自动生成模型文件并描述出各系统属性与事件流程；基于精化策略分层建模，对各层模型的证明义务进行定理证明，验证了系统的各项属性，得出可靠的通用功能模型；基于实例车站，对模型的公理进行了验证，同时实现了对联锁数据的确认；通过形式化验证过程，结合给定场景联锁数据的有效性确认，发现并纠正系统需求及分析过程中造成的潜在行为缺陷；通过功能仿真与验收测试，进一步确认了通用模型与联锁数据的正确性. 结果表明:本文方法提高了基于模型开发过程的准确性与层次性，验证了系统通用行为状态，且结合公理验证，实现了联锁数据的确认，并能基于模型进行功能场景仿真与测试，从而可进一步提高系统通用功能原型的可靠性. 

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

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.