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