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

Modeling and Verification of Typical FAO System Operation Scene Based on UPPAAL

作　　者：彭大天[1] 步兵[1] 

机构地区：[1]北京交通大学轨道交通控制与安全国家重点实验室

出　　处：《铁道学报》2013年第6期65-71,共7页Journal of the China Railway Society

基　　金：国家高技术研究发展计划(863计划)(2011AA110502);北京市科委项目(D111100000411001);中央高校基本科研业务费(2011JBZ014)

摘　　要：全自动驾驶系统FAO(Fully Automatic Operation)具有安全、可靠、高效的特点,成为未来城市轨道智能交通系统的主要发展方向。FAO系统典型运营场景是1个实时的过程,为发现其逻辑的错误、功能和性能的缺陷,需要在系统设计前,针对系统需求规范中典型运营场景的实现流程进行形式化分析。本文分析FAO典型运营场景保护区的实现流程,在系统需求规范中提取其功能与性能的需求,采用基于时间自动机理论的UPPAAL构建时间自动机网络模型,进行仿真分析,并验证其功能属性、性能属性与安全属性。通过反例分析、模型修正,增强对FAO系统的理解,减少设计故障,提高安全性,为系统设计与实现打下良好的基础。The fully automatic operation（FAO）system is characterized by high safety, high reliability and high efficiency,and it has become the main developing direction of the future urban rail intelligent transit sys- tem. The typical operation scene of the FAO System is a real time process. In order to find out logical systemat- ic inaccuracy and function and performance defects, the implementation process of the typical operation scene needs to be subjected to formalized analysis according to the specifications of system requirements before sys tern design. In this paper the implementation process of the typical FAO operation scene protected zone was an- alyzed,the function and performance requirements were extracted from the specifications of system requirements and the timed automata network model was built by UPPAAL based on the timed automata theo ry. Simulation analysis was made. Attributes of function, performance and safety were verified. Counter-example analysis and model updating may help to strengthen comprehension of the FAO System, reduce system design faults, improve safety of the FAO system and lay a good foundation for system design and execution.

关 键 词：全自动驾驶系统 保护区 UPPAAL 时间自动机 

分 类 号：U283[交通运输工程—交通信息工程及控制]