Verifying cooperative software: A SMT-based bounded model checking approach for deterministic scheduler

Cooperative software, such as SystemC multi-threaded software and OSEK/VDX multi-tasking application, has been widely applied for embedded systems. However, assuring high reliability of developed cooperative software has been a difficult problem as a result of the flexibly scheduling and complex cooperation in such software. Model checking has already shown its capability for cooperative software based on proposed verification techniques and hence has been regarded as a promising solution to solve the problem. However, the proposed model checking techniques are only interested in non-deterministic scheduler based cooperative software such as SystemC multi-threaded software so that they are usually unsuitable to verify the cooperative software under a deterministic scheduler. If the proposed model checking techniques are employed to verify this type of cooperative software such as OSEK/VDX mult-tasking applications, the verification is usually inexplicit since many superfluous interleavings of threads/tasks are taken into account in the verification stage. In this paper, we describe and develop a novel approach based on bounded model checking for the deterministic scheduler based cooperative software. We have evaluated our approach with a series of experiments. The experimental results indicate that our approach is a scalable and efficient technique for the deterministic scheduler based cooperative software.