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

作     者：华颖 张亚东 饶畅 胡智杰 王天成 张琳 徐坤 HUA Ying;ZHANG Ya-dong;RAO Chang;HU Zhi-jie;WANG Tian-cheng;ZHANG Lin;XU Kun

作者机构：西南交通大学信息科学与技术学院成都611756 

基　　金：中国铁路总公司科技研发课题(2016X001-C) 甘肃省高原交通信息工程及控制重点实验室项目(20161103) 西南交通大学SRTP项目(201610613096) 

出 版 物：《铁道标准设计》 (Railway Standard Design)

年 卷 期：2018年第62卷第4期

页      码：181-186页

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

主 题 词：时间自动机 二乘二取二 仿真 建模 验证 

学科分类：12[管理学] 1201[管理学-管理科学与工程类] 08[工学] 081201[081201] 082302[082302] 0812[工学-测绘类] 0823[工学-农业工程类] 

D　O　I：10.13238/j.issn.1004-2954.201704130004

馆 藏 号：203284629...