10.3969/j.issn.1001-8360.2011.06.012
基于时间自动机模型的安全计算机平台的形式化验证
众多工业控制领域要求计算机控制系统具有高可靠、高可用和高安全的运行基础,2乘2取2冗余结构的安全计算机平台是提高系统安全性、可靠性的一种重要解决方式.CBTC列控系统的安全计算机平台采用2乘2取2冗余结构,它是一个实时系统,控制过程需要考虑时间因素.本文分析CBTC系统安全计算机平台系统的组成结构,提取出系统的功能约束,采用基于时间自动机理论的建模验证工具UPPAAL建立系统的自动机网络模型,进行仿真分析,验证系统的功能性、实时性、安全性要求.
实时系统、安全计算机、时间自动机、模型验证、UPPAAL
33
TP301.1;TP319(计算技术、计算机技术)
国家科技支撑计划项目2006BAG02B04;北京市科技计划项目W06H0020
2011-09-26(万方平台首次上网日期,不代表论文的发表时间)
共6页
68-73