Efficient safety checking for automotive operating systems using property-based slicing and constraint-based environment generation

An automotive operating system is a safety-critical system that has a critical impact on the safety of road vehicles. Safety verification is a must in each stage of software development in such a system, but most existing work focuses on specification-level or model-level safety verification. This work proposes a collaborative approach using model checking and testing for the efficient safety checking of an automotive operating system. Efficiency is achieved through property-based slicing, which reduces the complexity of verification, and guided test sequence generation, which limits the input space to a set of representative test sequences selected from legal as well as illegal input spaces. Comprehensiveness is achieved by formally specifying external constraints using constraint automata from which guided test sequences are selected. The approach is implemented as a prototype tool set applied to the verification of an open source automotive operating system based on the OSEK/VDX international standard. The approach revealed several safety issues that could not be identified by existing approaches.