基于UPPAAL的二乘二取二逻辑建模与仿真

二乘二取二冗余结构以其高安全性和高可靠性特点,被广泛应用于核电、航空航天和铁路等安全关键领域。为验证二乘二取二冗余结构的核心逻辑,保证其高安全性和高可靠性的要求,对二乘二取二逻辑进行建模与验证。基于时间自动机理论,以列控车载ATP子系统二乘二取二冗余逻辑为研究对象,在分析工作原理的基础上,利用UPPAAL工具建立二乘二取二冗余逻辑的时间自动机模型,分别验证二乘、二取冗余逻辑的基本安全属性。根据验证后的软件逻辑模型,实现冗余逻辑仿真。模型构建与程序仿真的结果表明:车载ATP二乘二取二冗余逻辑结构具有高安全性与高可靠性。