دانلود مقاله ISI انگلیسی شماره 134864
ترجمه فارسی عنوان مقاله

مدل سازی رسمی و تایید سیستم های تکمیل شده با انتشار ترتیبی

عنوان انگلیسی
Formal modelling and verification of interlocking systems featuring sequential release
کد مقاله سال انتشار تعداد صفحات مقاله انگلیسی ترجمه فارسی
134864 2017 25 صفحه PDF سفارش دهید
دانلود فوری مقاله + سفارش ترجمه

نسخه انگلیسی مقاله همین الان قابل دانلود است.

هزینه ترجمه مقاله بر اساس تعداد کلمات مقاله انگلیسی محاسبه می شود.

این مقاله تقریباً شامل 17352 کلمه می باشد.

هزینه ترجمه مقاله توسط مترجمان با تجربه، طبق جدول زیر محاسبه می شود:

شرح تعرفه ترجمه زمان تحویل جمع هزینه
ترجمه تخصصی - سرعت عادی هر کلمه 12 تومان 25 روز بعد از پرداخت 208,224 تومان
ترجمه تخصصی - سرعت فوری هر کلمه 24 تومان 13 روز بعد از پرداخت 416,448 تومان
پس از پرداخت، فوراً می توانید مقاله را دانلود فرمایید.
منبع

Publisher : Elsevier - Science Direct (الزویر - ساینس دایرکت)

Journal : Science of Computer Programming, Volume 133, Part 2, 1 January 2017, Pages 91-115

پیش نمایش مقاله
پیش نمایش مقاله مدل سازی رسمی و تایید سیستم های تکمیل شده با انتشار ترتیبی

چکیده انگلیسی

In this article, we present a method and an associated toolchain for the formal verification of the new Danish railway interlocking systems that are compatible with the European Train Control System (ETCS) Level 2. We have made a generic and reconfigurable model of the system behaviour and generic safety properties. This model accommodates sequential release – a feature in the new Danish interlocking systems. To verify the safety of an interlocking system, first a domain-specific description of interlocking configuration data is constructed and validated. Then the generic model and safety properties are automatically instantiated with the well-formed description of interlocking configuration data. This instantiation produces a model instance in the form of a Kripke structure, and concrete safety properties expressed as invariants. Finally, using a combination of SMT based bounded model checking (BMC) and inductive reasoning, it is verified that the generated model instance satisfies the generated safety properties. Using this method, we are able to verify the safety properties for model instances corresponding to railway networks of industrial size. Experiments show that BMC is also efficient for finding bugs in the railway interlocking designs. Additionally, benchmarking results comparing the performance of our approach with alternative verification techniques on the interlocking models are presented.

دانلود فوری مقاله + سفارش ترجمه

نسخه انگلیسی مقاله همین الان قابل دانلود است.

هزینه ترجمه مقاله بر اساس تعداد کلمات مقاله انگلیسی محاسبه می شود.

این مقاله شامل 17352 کلمه می باشد.

هزینه ترجمه مقاله توسط مترجمان با تجربه، طبق جدول زیر محاسبه می شود:

شرح تعرفه ترجمه زمان تحویل جمع هزینه
ترجمه تخصصی - سرعت عادی هر کلمه 12 تومان 25 روز بعد از پرداخت 208,224 تومان
ترجمه تخصصی - سرعت فوری هر کلمه 24 تومان 13 روز بعد از پرداخت 416,448 تومان
پس از پرداخت، فوراً می توانید مقاله را دانلود فرمایید.