کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
6885389 | 1444510 | 2018 | 40 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
A configurable V&V framework using formal behavioral patterns for OSEK/VDX operating systems
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
شبکه های کامپیوتری و ارتباطات
پیش نمایش صفحه اول مقاله

چکیده انگلیسی
To assist in rigorous V&V activities for such embedded software, the proposed work suggests a pattern-based framework that can be used to generate configurable formal OS and test models. At the core of the framework, lies a set of predefined behavioral patterns and constraint patterns that can be composed for the auto-generation of formal models for variously configured operating systems. These configurable formal models form the basis of formal validation and verification activities such as model checking safety properties, model-based test generation, and formal application simulation. We have implemented a prototype tool, specially designed for embedded control software based on the OSEK/VDX international standard, to demonstrate the benefits of the framework in task simulation, test generation, and formal verification. A series of experiments and analysis demonstrate that the suggested pattern-based framework is more efficient in test sequence generation and more effective in identifying problems compared to existing approaches.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Systems and Software - Volume 137, March 2018, Pages 563-579
Journal: Journal of Systems and Software - Volume 137, March 2018, Pages 563-579
نویسندگان
Yunja Choi,