Model Checking Multitask Applications for OSEK Compliant Real-Time Operating Systems

In the verification of multitask software in real-time embedded systems, general purpose model checkers do not inherently consider characteristics of the real-time operating system, such as priority-based scheduling, priority inversion, and protocols for protecting shared memory resources. Since explicit state model checkers generally explore all possible execution paths and task interleaving, this could potentially lead to exploring execution paths that are redundant, unnecessarily increasing verification complexity and hampering tractability. Based on this premise, in this work we investigate how one can improve the performance of explicit state model checkers, such as SPIN, for the verification of multitask applications that target real-time operating systems.