Verifying scheduling point constraints with model checking

In this paper, we propose a method to verify whether a model is consistent to the scheduling point constraints in OSEK specification for non preemptive tasks. A simple operating system model is constructed and used to be the verification object. For verification, we build an auxiliary task set to interact with OS model, which makes the violation of scheduling point constraints appear. The property LTL formulae are generated from the constraints, which are verified by model checker SPIN. It is shown that our method can detect design mistakes.