Domain-Specific Language Facilitates Scheduling in Model Checking

A concurrent system consists of multiple processes that are run simultaneously. The execution orders of these processes are defined by a scheduler. In model checking techniques, the scheduling policy is closely related to a search algorithm that explores all of system states. To ensure the correctness of the system, the scheduling policy needs to be taken into account during the verification. Current approaches, which use fixed strategies, are only capable of limited kinds of policies and are difficult to extend to handle the variations of the schedulers. To address these problems, we propose a method using a domain-specific language (DSL) for the succinct specification of different scheduling policies. Necessary artifacts are automatically generated from the specification of the policy to analyze the system. We also propose a search algorithm for exploring the system states. Based on this method, we develop a tool to verify the system with different scheduling policies. Our experiments show that we could serve the variations of the schedulers easily and verify systems accurately.