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

摘要

全自动驾驶系统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 system.The typical operation scene of the FAO System is a real time process.In order to find out logical systematic 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 system design.In this paper the implementation process of the typical FAO operation scene protected zone was analyzed,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 theory.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.