软件学报

作者：赵梦瑶，陈小红，孙海英，刘静，陈良育，周庭梁

单位：赵梦瑶，上海市高可信计算重点实验室(华东师范大学), 上海 20006211,陈小红，上海市高可信计算重点实验室(华东师范大学), 上海 20006202,孙海英，上海市高可信计算重点实验室(华东师范大学), 上海 20006203,刘静，上海市高可信计算重点实验室(华东师范大学), 上海 20006204,陈良育，上海市高可信计算重点实验室(华东师范大学), 上海 20006205,周庭梁，卡斯柯信号有限公司, 上海 20007106

关键词：联锁系统|模板重用|形式化建模|随机混成自动机|领域特定语言

基金：国家重点研发计划（2018YFB2101300）；国家自然科学基金（61332008，91418203，61672230，61572195，11471209，61802251）；上海市经济和信息化委员会专项资金（160306）

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

来源：2020年第6期

《软件学报》期刊编辑部

查看软件学报杂志2020年第6期