@inproceedings{d724fa64e67040cfa88879e062cb8bab,
title = "Automating consistency verification of safety requirements for railway interlocking systems",
abstract = "Consistency verification of safety requirements is an important but still challenging task for safety-critical systems such as rail transit systems. That is mainly because requirements are typically written in natural language and with strong time constraints. Driven by the practical need from industry, in this paper we propose a systematic approach to specify safety requirements in a quasi-natural language and automatically verify their consistency using formal methods. Specifically, we define a domain specific language SafeNL to specify safety requirements, and then automatically transform them into formal constraints defined in the Clock Constraint Specification Language (CCSL). The transformed constraints can be automatically and efficiently verified by model checking. We conduct two practical case studies to analyze the safety requirements of an interlocking system in CASCO Signal Ltd. Results of the studies show the validity and utility of our approach can pragmatically contribute to industrial practice. We also report some lessons learned from case studies.",
keywords = "CCSL, Consistency Verification, Interlocking System, SafeNL, Safety Requirements",
author = "Xiaohong Chen and Zhiwei Zhong and Zhi Jin and Min Zhang and Tong Li and Xiang Chen and Tingliang Zhou",
note = "Publisher Copyright: {\textcopyright} 2019 IEEE.; 27th IEEE International Requirements Engineering Conference, RE 2019 ; Conference date: 23-09-2019 Through 27-09-2019",
year = "2019",
month = sep,
doi = "10.1109/RE.2019.00040",
language = "英语",
series = "Proceedings of the IEEE International Conference on Requirements Engineering",
publisher = "IEEE Computer Society",
pages = "308--318",
editor = "Daniela Damian and Anna Perini and Seok-Won Lee",
booktitle = "Proceedings - 2019 IEEE 27th International Requirements Engineering Conference, RE 2019",
address = "美国",
}