| 基于UPPAAL的列车自动防护系统形式化建模与验证 |
| |
| 引用本文： | 蒋建军,王长林. 基于UPPAAL的列车自动防护系统形式化建模与验证[J]. 铁路计算机应用, 2014, 23(8): 42-44 |
| |
| 作者姓名： | 蒋建军 王长林 |
| |
| 作者单位： | 西南交通大学 信息科学与技术学院,成都,610031 |
| |
| 摘 要： | 本文分析列车自动防护(ATP)系统的结构和功能需求,建立系统的时间自动机模型,采用UPPAAL模型验证工具对模型的活性和安全性进行验证.结果表明,采用时间自动机对安全苛求实时系统进行建模与验证,可以有效地保证系统的可靠性和实时性.
|
| 关 键 词： | 安全苛求系统 时间自动机 模型验证 UPPAAL |
| 收稿时间： | 2014-08-15 |
UPPAAL based modeling for Train Automatic Protection System |
| |
| JIANG Jianjun,WANG Changlin. UPPAAL based modeling for Train Automatic Protection System[J]. Railway Computer Application, 2014, 23(8): 42-44 |
| |
| Authors: | JIANG Jianjun WANG Changlin |
| |
| Affiliation: | ( School of Information Science and Technology, Chengdu 610031, China) |
| |
| Abstract: | 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. |
| |
| Keywords: | Safety Critical System timed automata model validation UPPAAL |
| 本文献已被 维普 等数据库收录！ |
| 点击此处可从《铁路计算机应用》浏览原始摘要信息 |
|
点击此处可从《铁路计算机应用》下载全文 |
