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

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.