کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
525119 868891 2014 16 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Formalizing a subset of ERTMS/ETCS specifications for verification purposes
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نرم افزارهای علوم کامپیوتر
پیش نمایش صفحه اول مقاله
Formalizing a subset of ERTMS/ETCS specifications for verification purposes
چکیده انگلیسی


• Literal ERTMS specifications can be subject to different interpretations.
• Formal notations are highly recommended when dealing with critical complex systems.
• A UML class-diagram has been developed to depict ERTMS/ETCS modes and transitions.
• ETCS modes and transitions' specifications are translated into a formal SMV model.
• Model-checking technique is shown to be efficient for ETCS specifications analysis.

ERTMS is the standard railway control-command and signaling system which aims to ensure railway interoperability throughout Europe while enhancing safety and competitiveness. ERTMS is composed of two main subsystems which include GSM-R, a radio system for enabling communication between the train and the traffic management center and ETCS, an automatic train protection system (ATP) to replace the existing national ATP systems. The ERTMS specifications are defined by means of standard documents which set out the requirements ensuring interoperability. These documents evolve regularly to give rise to successive versions. The ERTMS/ETCS standard defines different levels and operation modes according to various trackside and onboard setups and some operational conditions. Given the complexity and the high criticality of railway operation, verification and validation (V&V) are crucial tasks in railway application development.In this paper, after setting the background and the motivations, a mechanizable formalization of a subset of ERTMS/ETCS specifications relative to ETCS modes and transitions is developed. The present work aims to offer a readily available model for formal V&V. Using formal techniques to check SRS is highly recommended to tackle the complexity of the defined requirements and prevent specification errors. Model-checking technique, which is targeted here, offers exhaustive analysis of the system behavior based on its model and is highly automated, since it is supported by software tools. Based on the last available version of SRS specifications, a progressive process is undertaken to get a formal model which makes explicit the various modes characterized by their respective active functions, as well as the numerous combinations of conditions for switching between modes. The various steps guiding the translation of the SRS literal specifications into a formal model are explained. As will be shown through different examples, the obtained model is a convenient basis to check safety, interoperability and liveness properties.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Transportation Research Part C: Emerging Technologies - Volume 42, May 2014, Pages 60–75
نویسندگان
,