轨道交通联锁领域特定语言的形式化

• 作者: 刘静 周庭梁 孙海英 赵梦瑶 陈小红 陈良育
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 联锁系统 模板重用 形式化建模 随机混成自动机 领域特定语言
• 年，卷（期）: 2020,（6）
• 所属期刊栏目: 信息物理系统软件设计自动化专题
• 页码范围: 1638-1653
• 页数: 16页
• 分类号: TP311
• 字数: 14307字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005997

摘要

作为轨道交通系统的核心子系统之一,对联锁系统进行形式化建模与分析,是保证其安全性的重要手段.形式化建模需要领域知识和形式化知识的结合,由于形式化知识难以掌握,领域专家在建模整个过程中都需要形式化专家的帮助.为了解决这个问题,针对联锁系统的故障随机性、行为实时性、构件可重用的特点,提出设计联锁领域特定语言IS-DSL描述具体的联锁系统的参数,并基于随机混成自动机模板自动生成联锁系统的形式化模型,以进一步在此基础上进行安全分析.首先对联锁系统模型进行分析,根据不同案例设计其领域特定语言;其次,确定联锁系统的系统模型模板,包括环境构件模板和控制器模板,并举例抽取其随机混成自动机模板;在模板基础上定义系统模型生成过程,让领域专家可以通过领域特定语言,输入参数自动生成具体的随机混成自动机系统模型;最后以某站联锁系统为例,展示了基于模板的具体系统模型的生成过程,并通过基于系统模型的事故预测分析,证明了该方法的可行性与有效性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	周庭梁		16	68	4.0	8.0