کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
4956169 1444440 2017 26 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Verifying cooperative software: A SMT-based bounded model checking approach for deterministic scheduler
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر شبکه های کامپیوتری و ارتباطات
پیش نمایش صفحه اول مقاله
Verifying cooperative software: A SMT-based bounded model checking approach for deterministic scheduler
چکیده انگلیسی
Cooperative software, such as SystemC multi-threaded software and OSEK/VDX multi-tasking application, has been widely applied for embedded systems. However, assuring high reliability of developed cooperative software has been a difficult problem as a result of the flexibly scheduling and complex cooperation in such software. Model checking has already shown its capability for cooperative software based on proposed verification techniques and hence has been regarded as a promising solution to solve the problem. However, the proposed model checking techniques are only interested in non-deterministic scheduler based cooperative software such as SystemC multi-threaded software so that they are usually unsuitable to verify the cooperative software under a deterministic scheduler. If the proposed model checking techniques are employed to verify this type of cooperative software such as OSEK/VDX mult-tasking applications, the verification is usually inexplicit since many superfluous interleavings of threads/tasks are taken into account in the verification stage. In this paper, we describe and develop a novel approach based on bounded model checking for the deterministic scheduler based cooperative software. We have evaluated our approach with a series of experiments. The experimental results indicate that our approach is a scalable and efficient technique for the deterministic scheduler based cooperative software.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Systems Architecture - Volume 81, November 2017, Pages 7-16
نویسندگان
, , , , ,