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.