铁路信号安全关键软件形式化建模

• 作者: 李耀 杨扬 郭进 马亮
• 来源期刊: 铁道学报
• 学科: 交通运输
• 关键词: 安全关键软件 形式化建模 时钟约束 Timed SyncCharts Kripke 计算机联锁
• 年，卷（期）: 2017,（9）
• 所属期刊栏目: 铁道通信信号
• 页码范围: 74-80
• 页数: 7页
• 分类号: TP393|U283
• 字数: 7255字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-8360.2017.09.011

摘要

针对现行建模方法不能满足铁路信号系统安全关键软件的时钟约束需求和模型复杂度较高的问题,分析SyncCharts建模方法,针对其缺少形式化规范和时钟约束的问题,扩展出具有时钟属性的Timed SyncCharts建模方法.首先,采用Z语言系统地给出了Timed SyncCharts的形式化定义;其次,结合Timed SyncCharts的组件元素,确定Timed SyncCharts的宏步转移机制;然后,提出将Timed SyncCharts转化为Kripke结构的规则,保证了模型分析的可行性;最后,建立计算机联锁软件道岔定位需求的Timed SyncCharts模型,证明该方法的可行性和有效性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	郭进	西南交通大学信息科学与技术学院	122	918	16.0	23.0
2	马亮	西南交通大学信息科学与技术学院	13	139	6.0	11.0
3	李耀	西南交通大学信息科学与技术学院	16	57	5.0	7.0
4	杨扬	西南交通大学信息科学与技术学院	55	310	10.0	15.0