| 基于UPPAAL的FAO系统典型运营场景建模与验证 |
| |
| 引用本文： | 彭大天,步兵.基于UPPAAL的FAO系统典型运营场景建模与验证[J].铁道学报,2013(6):65-71. |
| |
| 作者姓名： | 彭大天 步兵 |
| |
| 作者单位： | 北京交通大学轨道交通控制与安全国家重点实验室 |
| |
| 基金项目： | 国家高技术研究发展计划(863计划)(2011AA110502);北京市科委项目(D111100000411001);中央高校基本科研业务费(2011JBZ014) |
| |
| 摘 要： | 全自动驾驶系统FAO(Fully Automatic Operation)具有安全、可靠、高效的特点,成为未来城市轨道智能交通系统的主要发展方向。FAO系统典型运营场景是1个实时的过程,为发现其逻辑的错误、功能和性能的缺陷,需要在系统设计前,针对系统需求规范中典型运营场景的实现流程进行形式化分析。本文分析FAO典型运营场景保护区的实现流程,在系统需求规范中提取其功能与性能的需求,采用基于时间自动机理论的UPPAAL构建时间自动机网络模型,进行仿真分析,并验证其功能属性、性能属性与安全属性。通过反例分析、模型修正,增强对FAO系统的理解,减少设计故障,提高安全性,为系统设计与实现打下良好的基础。
|
| 关 键 词： | 全自动驾驶系统 保护区 UPPAAL 时间自动机 |
| 本文献已被 CNKI 等数据库收录！ |
|
