SSpinJa: Facilitating Schedulers in Model Checking

The execution of a software system that runs on top of an Operating System (OS) is usually controlled by the scheduler. Therefore, to accurately verify the system, the scheduling policy needs to be taken into account in the verification. In model checking techniques, the scheduling policy affects the search algorithm to explore the state space to check the behaviors of the system. Existing works try to specify/implement the scheduler(s) along with the set of processes in the specification language(s) used by the model checking tool(s). In reality, many kinds of scheduling policies are used by the OS(s), e.g. round-robin, priority, and first-in-first-out. There are also many variations of these policies, which are usually different from the 'textbook’ ones. That means dealing with the variations of the scheduling policies in model checking is necessary and important. However, because the implementation of the scheduler always starts from scratch, it is error-prone and time-consuming. Therefore, the existing works are difficult to deal with the different scheduling policies. To address this problem, we propose a method that introduces a domain-specific language (DSL) to facilitate the variation of the policies. All necessary information to perform the scheduling tasks is generated automatically from the description of the scheduler. We also introduce a search algorithm using this information to explore the states of the system to verify the behaviors of the system. In this paper, we introduce SSpinJa, a tool in which we implemented this approach. Our tool supports an environment for editing the scheduling policy (in the DSL) and the model checker for verifying the system. The results of our experiments show that a) we can handle different scheduling policies easily, b) we can accurately verify the behaviors of the systems, and c) our approach is also practical.