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

• 作者: 王长林 蒋建军
• 来源期刊: 铁路计算机应用
• 学科: 交通运输
• 关键词: 安全苛求系统 时间自动机 模型验证 UPPAAL
• 年，卷（期）: 2014,（8）
• 所属期刊栏目: 计算机与通信信号
• 页码范围: 42-44,48
• 页数: 4页
• 分类号: U284.48|TP39
• 字数: 3114字
• 语种: 中文

摘要

本文分析列车自动防护(ATP)系统的结构和功能需求,建立系统的时间自动机模型,采用UPPAAL模型验证工具对模型的活性和安全性进行验证.结果表明,采用时间自动机对安全苛求实时系统进行建模与验证,可以有效地保证系统的可靠性和实时性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王长林	西南交通大学信息科学与技术学院	67	573	13.0	20.0
2	蒋建军	西南交通大学信息科学与技术学院	2	5	1.0	2.0