基于UPPAAL的FAO系统典型运营场景建模与验证

• 作者: 彭大天 步兵
• 来源期刊: 铁道学报
• 学科: 交通运输
• 关键词: 全自动驾驶系统 保护区 UPPAAL 时间自动机
• 年，卷（期）: 2013,（6）
• 所属期刊栏目: 铁道通信信号
• 页码范围: 65-71
• 页数: 7页
• 分类号: U283
• 字数: 4778字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-8360.2013.06.011

摘要

全自动驾驶系统FAO(Fully Automatic Operation)具有安全、可靠、高效的特点,成为未来城市轨道智能交通系统的主要发展方向.FAO系统典型运营场景是1个实时的过程,为发现其逻辑的错误、功能和性能的缺陷,需要在系统设计前,针对系统需求规范中典型运营场景的实现流程进行形式化分析.本文分析FAO典型运营场景保护区的实现流程,在系统需求规范中提取其功能与性能的需求,采用基于时间自动机理论的UPPAAL构建时间自动机网络模型,进行仿真分析,并验证其功能属性、性能属性与安全属性.通过反例分析、模型修正,增强对FAO系统的理解,减少设计故障,提高安全性,为系统设计与实现打下良好的基础.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	彭大天	北京交通大学轨道交通控制与安全国家重点实验室	1	8	1.0	1.0
2	步兵	北京交通大学轨道交通控制与安全国家重点实验室	7	80	5.0	7.0