轨道交通联锁领域特定语言的形式化-赵梦瑶，陈小红，孙海英，刘静，陈良育，周庭梁.pdf
免费下载
软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
Journal of Software,2020,31(6):1638−1653 [doi: 10.13328/j.cnki.jos.005997] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563
轨道交通联锁领域特定语言的形式化
∗
赵梦瑶
1
,
陈小红
1
,
孙海英
1
,
刘
静
1
,
陈良育
1
,
周庭梁
2
1
(上海市高可信计算重点实验室(华东师范大学),上海 200062)
2
(卡斯柯信号有限公司,上海 200071)
通讯作者: 陈小红, E-mail: xhch en@s ei.ecn u.edu. cn
摘 要: 作为轨道交通系统的核心子系统之一,对联锁系统进行形式化建模与分析,是保证其安全性的重要手段.
形式化建模需要领域知识和形式化知识的结合,由于形式化知识难以掌握,领域专家在建模整个过程中都需要形式
化专家的帮助.为了解决这个问题,针对联锁系统的故障随机性、行为实时性、构件可重用的特点,提出设计联锁领
域特定语言 IS-DSL 描述具体的联锁系统的参数,并基于随机混成自动机模板自动生成联锁系统的形式化模型,以
进一步在此基础上进行安全分析.首先对联锁系统模型进行分析,根据不同案例设计其领域特定语言;其次,确定联
锁系统的系统模型模板,包括环境构件模板和控制器模板,并举例抽取其随机混成自动机模板;在模板基础上定义系
统模型生成过程,让领域专家可以通过领域特定语言,输入参数自动生成具体的随机混成自动机系统模型;最后以某
站联锁系统为例,展示了基于模板的具体系统模型的生成过程,并通过基于系统模型的事故预测分析,证明了该方法
的可行性与有效性.
关键词: 联锁系统;模板重用;形式化建模;随机混成自动机;领域特定语言
中图法分类号: TP311
中文引用格式: 赵梦瑶,陈小红,孙海英,刘静,陈良育,周庭梁.轨道交通联锁领域特定语言的形式化.软件学报,2020,31(6 ):
1638−1653. http ://www.jos.org.cn/1000-9825/5997.htm
英文引用格式: Zhao MY, Chen XH, Sun HY, Liu J, Chen LY, Zhou TL. Formalizing railway interlocking domain specific
language. Ruan Jian Xue Bao/Journal of Software, 2020,31(6):1638−1653 (in Chinese). http://www.jos.org.cn/1000-9825/5997.
htm
Formalizing Railway Interlocking Domain Specific Language
ZHAO Meng-Yao
1
, CHEN Xiao-Hong
1
, SUN Hai-Ying
1
, LIU Jing
1
, CHEN Liang-Yu
1
, ZHOU Ting-Liang
2
1
(Shanghai Key Laboratory of Trustworthy Computing (East China Normal University), Shanghai 200062, China)
2
(Casco Signal Co. Ltd., Shanghai 200071, Chin a)
Abstra ct : 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. For malization requires both domain knowledge and for mal knowl edge. Sin ce for mal 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, r eal-time behavior, and reusability of components in railway int erlocking 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
∗ 基金项目: 国家重点研发计划(2018YFB2101300); 国家自然科学基金(61332008, 91418203, 61672230, 61572195, 11471209,
61802251); 上海市经济和信息化委员会专项资金(160306)
Foundation item: National Key R&D Program of China (2018YFB2101300); National Natural Science Foundation of China
(61332008, 91418203, 61672230, 61572195, 11471209, 61802251); Sp ecific Foundation of Shanghai Municipal Commission of Economy
and Informatization (160306)
本文由“信息物理系统软件设计自动化”专题特约编辑卜磊教授、陈铭松教授、朱祺教授、刘超教授推荐.
收稿时间: 2019-08-20; 修改时间: 2019-10-23; 采用时间: 2020-01-13
赵梦瑶 等:轨道交通联锁领域特定语言的形式化
1639
interlocking system is analyzed firstl y, and the domain specific language is designed accord ing 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 extr acted as examples. Based on these te mplates, the system model generation p rocess is defined, so th at 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 propos ed approach .
Key words: interlocking system; template reuse; formal modeling; stochastic hybrid automata (SHA); domain specific language
轨道交通联锁系统是以计算机、现代多媒体和通信网络技术等技术为手段,以道岔机、信号机和轨道电路
作为基础设备,主要负责处理进路内的信号机、道岔、轨道电路之间的安全联锁关系
[1]
.它包括实现联锁关系、
建立进路、控制道岔的转换和信号灯的开放以及进路解锁,是轨道交通信号系统中不可或缺的核心部分,是保
证列车行车安全的重要子系统.它有欧盟安全完整性等级最高的 SIL4 级安全需求
[2]
、复杂的逻辑和很高的实
时性能,若发生故障,则能危害整列车的安全.因此,必须确保联锁系统的高安全性.
为了保证这样的安全性,目前很多欧洲铁路控制与防护标准,如 EN50128
[2]
,EN50129
[3]
等强烈推荐在开发
之前,使用形式化方法进行建模和分析.形式化方法以严密的数学理论和相关推理为基础,有严格的语法规范和
确定的语义定义,并且是自证正确的,因此非常适用于开发联锁系统这样安全攸关的系统.但是,形式化方法又
有着固有的学习成本高、不易使用的缺点.一般来说,领域专家的形式化建模离不开形式化专家的帮助,建模的
主体依然是形式化的专家.在联锁系统这类领域知识特别复杂的系统中,领域专家需要快速构建模型并分析复
杂业务逻辑,根据分析结果快速进行错误定位与错误修正,建模与分析的主体应该是领域专家.如何让领域专家
能自主构建形式化模型,是一个需要解决的问题.
现有的轨道交通领域的形式化建模工作主要分为 3 类:基于自然语言的形式化方法、基于半形式化的方法
和基于领域特定语言(DSL)的方法.基于自然语言的形式化建模
[4−6]
都是形式化专家根据领域专家的自然语言
描述直接建立形式化模型,并采用相应的形式化验证工具进行性质验证,这类方法需要领域专家和形式化专家
的紧密合作,对于不具有形式化知识的领域专家来讲很难使用.基于半形式化的形式化建模与验证中
[7−11]
,先由
领域专家使用半形式化语言(例如 UML)描述系统,然后形式化专家再把半形式化模型转换为形式化模型并进
行形式化分析.但这些半形式化语言都是软件专业建模语言,不是领域专家所擅长的语言.基于领域特定语言的
形式化建模与验证中
[12−15]
,首先由领域专家使用领域特定语言描述系统,然后形式化专家再把领域特定语言模
型转换为形式化模型并进行形式化分析.例如,Idani 等人
[12]
将图形领域定制语言的模型转换为形式化 B 模型.
这类方法允许领域专家只要根据领域特定语言给出领域模型,就可以享受形式化方法带来的好处,便于形式化
专家和领域专家的合作,也减少了人工建模出错误的可能性.
基于以上分析,我们认为,基于领域特定语言的建模方法更方便领域专家使用.但现有的基于特定语言的方
法并不能直接应用于联锁系统,原因如下:
(1) 使用的形式化模型,如文献[12]使用的 B 方法和文献[13]使用的时间弧 Petri 网等,并不能应对联锁系
统的故障随机性和行为实时性的特点.联锁系统中,事故通常是由设备故障造成的,而设备故障通常
具有随机性的特点,例如由雷击等意外事件导致轨道电路出现短路等故障.同时,联锁系统属于典型
的实时系统,逻辑复杂且有较高的实时性要求
[16]
;
(2) 可重用构件多,需要多次重用列车、轨道等构件.联锁系统在各个站的组成都类似,每个站的联锁系统
都有着相同的构件,如列车、轨道、道岔、信号灯、联锁表、控制器,它们的主要区别在于车站布局(车
站站场图)不同导致的实例个数不同.
因此,在前期工作基础上
[14,15]
,本文提出了基于模板的联锁系统模型生成方法,建立联锁系统的特定领域语
言,通过模板重用,允许领域专家根据实际需要自行构建系统模型,而不必接受形式化方法的培训.这种模板可
以用能建模故障随机性和实时性的随机混成自动机
[17]
或价格时间自动机
[18]
进行构建.
本文首先由领域专家对联锁系统模型进行分析,根据不同案例设计其领域特定语言;其次,由领域专家确定
of 16
免费下载
【版权声明】本文为墨天轮用户原创内容，转载时必须标注文档的来源（墨天轮），文档链接，文档作者等基本信息，否则作者和墨天轮有权追究责任。如果您发现墨天轮中有涉嫌抄袭或者侵权的内容，欢迎发送邮件至：contact@modb.pro进行举报，并提供相关证据，一经查实，墨天轮将立刻删除相关内容。
下载排行榜
评论