主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2020-2021年专刊出版计划 微信服务介绍 最新一期:2020年第7期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
赵梦瑶,陈小红,孙海英,刘静,陈良育,周庭梁.轨道交通联锁领域特定语言的形式化.软件学报,2020,31(6):1638-1653
轨道交通联锁领域特定语言的形式化
Formalizing Railway Interlocking Domain Specific Language
投稿时间:2019-08-20  修订日期:2019-10-23
DOI:10.13328/j.cnki.jos.005997
中文关键词:  联锁系统|模板重用|形式化建模|随机混成自动机|领域特定语言
英文关键词:interlocking system|template reuse|formal modeling|stochastic hybrid automata (SHA)|domain specific language
基金项目:国家重点研发计划(2018YFB2101300);国家自然科学基金(61332008,91418203,61672230,61572195,11471209,61802251);上海市经济和信息化委员会专项资金(160306)
作者单位E-mail
赵梦瑶 上海市高可信计算重点实验室(华东师范大学), 上海 200062  
陈小红 上海市高可信计算重点实验室(华东师范大学), 上海 200062 xhchen@sei.ecnu.edu.cn 
孙海英 上海市高可信计算重点实验室(华东师范大学), 上海 200062  
刘静 上海市高可信计算重点实验室(华东师范大学), 上海 200062  
陈良育 上海市高可信计算重点实验室(华东师范大学), 上海 200062  
周庭梁 卡斯柯信号有限公司, 上海 200071  
摘要点击次数: 514
全文下载次数: 749
中文摘要:
      作为轨道交通系统的核心子系统之一,对联锁系统进行形式化建模与分析,是保证其安全性的重要手段.形式化建模需要领域知识和形式化知识的结合,由于形式化知识难以掌握,领域专家在建模整个过程中都需要形式化专家的帮助.为了解决这个问题,针对联锁系统的故障随机性、行为实时性、构件可重用的特点,提出设计联锁领域特定语言IS-DSL描述具体的联锁系统的参数,并基于随机混成自动机模板自动生成联锁系统的形式化模型,以进一步在此基础上进行安全分析.首先对联锁系统模型进行分析,根据不同案例设计其领域特定语言;其次,确定联锁系统的系统模型模板,包括环境构件模板和控制器模板,并举例抽取其随机混成自动机模板;在模板基础上定义系统模型生成过程,让领域专家可以通过领域特定语言,输入参数自动生成具体的随机混成自动机系统模型;最后以某站联锁系统为例,展示了基于模板的具体系统模型的生成过程,并通过基于系统模型的事故预测分析,证明了该方法的可行性与有效性.
英文摘要:
      As a core subsystem of the rail transit systems, the formal modeling and analysis of the interlocking system is an important means to ensure its safety. Formalization requires both domain knowledge and formal knowledge. Since formal knowledge is difficult to master, domain experts need the help of formal experts throughout the modeling process. To solve this problem, aiming at the characteristics of fault randomness, real-time behavior, and reusability of components in railway interlocking systems, a specific language IS-DSL is proposed to describe the parameters of specific interlocking system. A formal model of interlocking system is generated automatically based on the stochastic hybrid automata (SHA) templates, to carry out further safety analysis. In this study, the model of interlocking system is analyzed firstly, and the domain specific language is designed according to different cases. Secondly, the templates of the interlocking system model, including environment component templates and controller template are established, and the SHA templates are extracted as examples. Based on these templates, the system model generation process is defined, so that the domain experts can automatically generate the specific SHA model by inputting parameters through the IS-DSL. Finally, the interlocking system of a station is taken as an example to show the generation process. The following accident prediction analysis based on this system model proves the feasibility and effectiveness of the proposed approach.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利