基于时间自动机模型的安全计算机平台的形式化验证

众多工业控制领域要求计算机控制系统具有高可靠、高可用和高安全的运行基础,2乘2取2冗余结构的安全计算机平台是提高系统安全性、可靠性的一种重要解决方式。CBTC列控系统的安全计算机平台采用2乘2取2冗余结构,它是一个实时系统,控制过程需要考虑时间因素。本文分析CBTC系统安全计算机平台系统的组成结构,提取出系统的功能约束,采用基于时间自动机理论的建模验证工具UPPAAL建立系统的自动机网络模型,进行仿真分析,验证系统的功能性、实时性、安全性要求。

Formal Verification of Safety Computer Platform Based on Timed Automata Model

In many industrial control fields,the running foundation of the computer control system is required to be highly reliable,available and safe.Using the 2×2-out-of-2 redundant structure to form the safety computer platform is an important solution to improve security and reliability of the computer control system.The safety computer platform of the CBTC trains control system uses the 2×2-out-of-2 structure which is a real-time system,taking the time factor into account in the control process.The structure of the safety computer system is analyzed and the function of the system is extracted.The timed automata network model of the system is built using the validation tool UPPAAL on the basis of the timed automata theory.Then simulation is carried out to verify,the functionality and the real-time and safety properties of the system.