کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
6875285 | 1441594 | 2018 | 28 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Verification of the European Rail Traffic Management System in Real-Time Maude
ترجمه فارسی عنوان
تأیید سیستم مدیریت ترافیک راه آهن اروپا در زمان واقعی
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
چکیده انگلیسی
The approach given in this paper is a rigorous one. In order to avoid modelling errors, we follow a systematic approach: First, as a requirement specification, we identify the event-response structures present in the ERTMS. Then, we model these structures in Real-Time Maude in a traceable way, i.e., specification text in Real-Time Maude can be directly mapped to requirements. We explore our models by checking if they have the desired behaviour, and apply systematic model-exploration through error injection - both these steps are carried out using the formal method Real-Time Maude. Finally, we analyse ERTMS by model-checking, thus applying a formal method to the railway domain, and we mathematically prove that our analysis of ERTMS by model-checking is complete, i.e., that it guarantees safety at all times.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Science of Computer Programming - Volume 154, 1 March 2018, Pages 61-88
Journal: Science of Computer Programming - Volume 154, 1 March 2018, Pages 61-88
نویسندگان
Ulrich Berger, Phillip James, Andrew Lawrence, Markus Roggenbach, Monika Seisenberger,