铁道标准设计2018，Vol.62Issue(4)：181-186,6.DOI:10.13238/j.issn.1004-2954.201704130004
基于UPPAAL的二乘二取二逻辑建模与仿真
Logical Modeling and Simulation of Double 2-vote-2 Redundant Structure Based on UPPAAL
摘要
Abstract
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.关键词
时间自动机/二乘二取二/仿真/建模/验证Key words
Timed automata/Double 2-vote-2/Simulation/Modeling/Verification分类
信息技术与安全科学引用本文复制引用
华颖,张亚东,饶畅,胡智杰,王天成,张琳,徐坤..基于UPPAAL的二乘二取二逻辑建模与仿真[J].铁道标准设计,2018,62(4):181-186,6.基金项目
中国铁路总公司科技研发课题(2016X001-C) （2016X001-C）
甘肃省高原交通信息工程及控制重点实验室项目(20161103) （20161103）
西南交通大学SRTP项目(201610613096) （201610613096）
