کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4956169 | 1444440 | 2017 | 26 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Verifying cooperative software: A SMT-based bounded model checking approach for deterministic scheduler
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
شبکه های کامپیوتری و ارتباطات
پیش نمایش صفحه اول مقاله
چکیده انگلیسی
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
Journal: Journal of Systems Architecture - Volume 81, November 2017, Pages 7-16
نویسندگان
Haitao Zhang, Guoqiang Li, Daniel Sun, Yonggang Lu, Ching-Hsien Hsu,