摘要
二乘二取二冗余结构以其高安全性和高可靠性特点,被广泛应用于核电、航空航天和铁路等安全关键领域。为验证二乘二取二冗余结构的核心逻辑,保证其高安全性和高可靠性的要求,对二乘二取二逻辑进行建模与验证。基于时间自动机理论,以列控车载ATP子系统二乘二取二冗余逻辑为研究对象,在分析工作原理的基础上,利用UPPAAL工具建立二乘二取二冗余逻辑的时间自动机模型,分别验证二乘、二取冗余逻辑的基本安全属性。根据验证后的软件逻辑模型,实现冗余逻辑仿真。模型构建与程序仿真的结果表明:车载ATP二乘二取二冗余逻辑结构具有高安全性与高可靠性。
Double 2-vote-2 redundant structure of high security and reliability is widely used in such security-intensive fields as nuclear power,aerospace and railway. To verify double 2-vote-2 redundant structure＇s core logic and guarantee its high security and reliability,this paper establishes and verifies double 2-vote-2 redundant structure models. Based on timed automata theory, train control system vehicle-mounted ATP subsystem ＇s double 2-vote-2 redundant logic and the analysis of its working principles,this paper employs UPPAAL tool to build double 2-vote-2 redundant logical timed automata models and verifies respectively two-by-two and two-vote-two logical basic security properties. Redundant logical simulation is conducted by means of verified logical models. The results of modeling and program simulation show that vehicle-mounted ATP double 2-vote-2 redundant logical structure is safe and reliable.
作者
华颖
张亚东
饶畅
胡智杰
王天成
张琳
徐坤
HUA Ying;ZHANG Ya-dong;RAO Chang;HU Zhi-jie;WANG Tian-cheng;ZHANG Lin;XU Kun(School of Information Science and Technology,Southwest Jiaotong University,Chengdu 611756, China)
出处
《铁道标准设计》
北大核心
2018年第4期181-186,共6页
Railway Standard Design
基金
中国铁路总公司科技研发课题(2016X001-C)
甘肃省高原交通信息工程及控制重点实验室项目(20161103)
西南交通大学SRTP项目(201610613096)
关键词
时间自动机
二乘二取二
仿真
建模
验证
Timed automata
Double 2-vote-2
Simulation
Modeling
Verification
