基于UPPAAL的列车自动防护系统形式化建模与验证  

UPPAAL based modeling for Train Automatic Protection System

作　　者：蒋建军[1] 王长林[1] 

机构地区：[1]西南交通大学信息科学与技术学院,成都610031

出　　处：《铁路计算机应用》2014年第8期42-44,48,共4页Railway Computer Application

摘　　要：本文分析列车自动防护(ATP)系统的结构和功能需求,建立系统的时间自动机模型,采用UPPAAL模型验证工具对模型的活性和安全性进行验证。结果表明,采用时间自动机对安全苛求实时系统进行建模与验证,可以有效地保证系统的可靠性和实时性。This paper analyzed the structure and functional requirements of Train Automatic Protection（ATP） System,set up a timed automata model,activity and safety of the model was verified by using the UPPAAL model verification tool.The results showed that,using timed automata to model and analyze the safety critical real-time systems,could provide effective guarantee for the real-time and reliability of the System.

关 键 词：安全苛求系统 时间自动机 模型验证 UPPAAL 

分 类 号：U284.48[交通运输工程—交通信息工程及控制] TP39[交通运输工程—道路与铁道工程]