Conformance Testing of Schedulers for DSL-based Model Checking

When we verify concurrent systems executed under a real operating system (OS), we should take the scheduling policy of the OS into account. However, with a specific implementation of an OS, the description of the scheduling policy does not exist or not clear to describe the behaviors of the real scheduler. In this case, we need to make assumptions in the specification by ourselves. Therefore, checking the correctness of the specification of the scheduling policy is important because it affects the verification result. In this paper, we propose a method to validate the correspondence between the specification of the scheduling policy and the implementation of the scheduler using testing techniques. The overall approach can be regarded as conformance testing. As a result, we can find the inconsistency between the implementation and the specification. That indicates the incorrectness of the specification. To deal with testing, we propose a domain-specific language (DSL) to specify the test generation with the scheduling policy. A search algorithm is introduced to determine the executions of the processes. The tests are generated automatically and exhaustively by applying model-based testing (MBT) techniques. Based on this method, we develop a tool for generating the tests. We demonstrate our method with Linux FIFO scheduling policy. The experiments show that we can facilitate the test generation and check the specification of the scheduling policy easily.