کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
433201 1441621 2016 20 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Validation process for railway interlocking systems
ترجمه فارسی عنوان
پروتکل اعتبارسنجی برای سیستم های متصل کردن راه آهن
کلمات کلیدی
سیستم های متصل کردن راه آهن؛ اعتبار سیستم؛ تست مبتنی بر مدل؛ روش های رسمی؛ چک کردن مدل
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
چکیده انگلیسی


• We address railway interlocking system validation by means of model-based techniques.
• We extract a model from the produced application and we use the model for testing.
• We also use the model for formal verification by model checking.

An interlocking system monitors the status of the objects in a railway yard, allowing or denying the movement of trains, in accordance with safety rules. The high number of complex interlocking rules that guarantee the safe movements of independent trains in a large station makes the verification of such systems a complex task, which needs to be addressed in conformance with EN50128 safety guidelines.In this paper we show how the problem has been addressed by a manufacturer at the final validation stage of production interlocking systems, by means of a model extraction procedure that creates a model of the internal behaviour, to be exercised with the planned test suites, in order to reduce the high costs of direct validation of the target system.The same extracted model is then subject to formal verification experiments, employing an iterative verification process implementing slicing and CEGAR-like techniques, defined to address the typical complexity of this application domain.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Science of Computer Programming - Volume 128, 15 October 2016, Pages 2–21
نویسندگان
, , , ,