Model checking embedded control software using OS-in-the-loop CEGAR

Verification of multitasking embedded software requires taking into account its underlying operating system w.r.t. its scheduling policy and handling of task priorities in order to achieve a higher degree of accuracy. However, such comprehensive verification of multitasking embedded software together with its underlying operating system is very costly and impractical. To reduce the verification cost while achieving the desired accuracy, we propose a variant of CEGAR, named OiL-CEGAR (OS-in-the-Loop Counterexample-Guided Abstraction Refinement), where a composition of a formal OS model and an abstracted application program is used for comprehensive verification and is successively refined using the counterexamples generated from the composition model. The refinement process utilizes the scheduling information in the counterexample, which acts as a mini-OS to check the executability of the counterexample trace on the concrete program. Our experiments using a prototype implementation of OiL-CEGAR show that OiL-CEGAR greatly improves the accuracy and efficiency of property checking in this domain. It automatically removed all false alarms and accomplished property checking within an average of 476 seconds over a set of multitasking programs, whereas model checking using existing approaches over the same set of programs either showed an accuracy of under 11.1% or was unable to finish the verification due to timeout.