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

چک کردن کامل مدل TCTL نمادین برای سیستم های بی درنگ کامل و ناقص

کد مقاله سال انتشار مقاله انگلیسی ترجمه فارسی تعداد کلمات
43094 2015 29 صفحه PDF سفارش دهید محاسبه نشده
خرید مقاله
پس از پرداخت، فوراً می توانید مقاله را دانلود فرمایید.
عنوان انگلیسی
Fully symbolic TCTL model checking for complete and incomplete real-time systems ☆☆☆
منبع

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

Journal : Science of Computer Programming, Volume 111, Part 2, 1 November 2015, Pages 248–276

کلمات کلیدی
اتوماسیون زمان بندی شده - سیستم های بی درنگ ناقص - چک کردن کامل مدل TCTL
پیش نمایش مقاله
پیش نمایش مقاله چک کردن کامل مدل TCTL نمادین برای سیستم های بی درنگ کامل و ناقص

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

In this paper we present a fully symbolic TCTL model checking algorithm for real-time systems represented in a formal model called finite state machine with time (FSMT), which works on fully symbolic state sets containing both the clock values and the state variables. Our algorithm is able to verify TCTL properties on complete and incomplete FSMTs containing unknown components. For that purpose over-approximations of state sets fulfilling a TCTL property ϕ for at least one implementation of the unknown components and under-approximations of state sets fulfilling ϕ for all possible implementations of the unknown components are computed. We present two different methods to convert timed automata to FSMTs. In addition to FSMTs simulating pure interleaving behaviour of timed automata we can produce FSMTs with a parallelized interleaving behaviour which allows parallelism of conflict-free transitions. This can dramatically reduce the number of steps during verification. Our prototype implementation outperforms the state-of-the-art model checkers UPPAAL and RED on complete systems, and on incomplete systems our tool is able to prove interesting properties when parts of the system are unknown.

خرید مقاله
پس از پرداخت، فوراً می توانید مقاله را دانلود فرمایید.