Model Checking in the Presence of Schedulers Using a Domain-Specific Language for Scheduling Policies
-
- TRAN Nhat-Hoa
- Software Engineering Department, National University of Civil Engineering
-
- CHIBA Yuki
- Advanced R & D Dept., Tokyo Office, DENSO CORPORATION
-
- AOKI Toshiaki
- School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)
抄録
<p>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 the search algorithm that explores all of the 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 to analyze the behaviors of the system. We also propose a search algorithm for exploring the state space. Based on this method, we develop a tool to verify the system with the scheduler. Our experiments show that we could serve the variations of the schedulers easily and verify the systems accurately.</p>
収録刊行物
-
- IEICE Transactions on Information and Systems
-
IEICE Transactions on Information and Systems E102.D (7), 1280-1295, 2019-07-01
一般社団法人 電子情報通信学会
- Tweet
詳細情報 詳細情報について
-
- CRID
- 1390564238104446080
-
- NII論文ID
- 130007671332
-
- ISSN
- 17451361
- 09168532
-
- 本文言語コード
- en
-
- データソース種別
-
- JaLC
- Crossref
- CiNii Articles
- KAKEN
-
- 抄録ライセンスフラグ
- 使用不可