Formalizing Railway Interlocking Domain Specific Language
Author:
Affiliation:

Clc Number:

Fund Project:

National Key R&D Program of China (2018YFB2101300); National Natural Science Foundation of China (61332008, 91418203, 61672230, 61572195, 11471209, 61802251); Specific Foundation of Shanghai Municipal Commission of Economy and Informatization (160306)

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    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.

    Reference
    Related
    Cited by
Get Citation

赵梦瑶,陈小红,孙海英,刘静,陈良育,周庭梁.轨道交通联锁领域特定语言的形式化.软件学报,2020,31(6):1638-1653

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:August 20,2019
  • Revised:October 23,2019
  • Adopted:
  • Online: April 20,2020
  • Published: June 06,2020
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063