基于TSSM的城市轨道交通CBTC区域控制器建模与验证

• 作者: 周正 孔令晶 李耀 郭进 陈荣武
• 来源期刊: 西南交通大学学报
• 学科: 交通运输
• 关键词: 区域控制器 时间安全状态机 建模 高安全性应用开发环境 验证 模型检测
• 年，卷（期）: 2015,（1）
• 页码范围: 27-35
• 页数: 9页
• 分类号: TP393|U283
• 字数: 5992字
• 语种: 中文
• DOI: 10.3969/j.issn.0258-2724.2015.01.005

摘要

针对安全状态机缺乏时间描述能力的缺点,利用反应式系统的同步设计方法,提出了时间安全状态机TSSM(timed safe state machine)建模方法,定义了弱变迁和同步变迁语法,建立了城市轨道交通ZC(zone controller)系统模型.首先,分析了ZC系统的运行环境、工作原理和功能需求,根据ZC反应式系统的特点,利用TSSM在SCADE(safety critical application development environment)中建立了ZC系统列车管理、ZC控制、MA计算和队列管理子模型;其次,通过ZC系统的TSSM网络模型,分析了子模型间的交互信息;最后,采用Lustre语言对ZC系统的安全特性进行了形式化描述,并利用Design Verifier模型检测工具,结合数据流验证了ZC系统的功能和性能需要.研究结果表明,ZC系统TSSM模型的安全性和受限活性均为有效,ZC系统完全满足预期的安全需求.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	郭进	西南交通大学信息科学与技术学院	122	918	16.0	23.0
2	李耀	西南交通大学信息科学与技术学院	16	57	5.0	7.0
3	陈荣武	西南交通大学信息科学与技术学院	27	259	7.0	15.0
4	孔令晶	西南交通大学信息科学与技术学院	6	23	3.0	4.0
5	周正	西南交通大学信息科学与技术学院	1	9	1.0	1.0