The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. ex. Some numerals are expressed as "XNUMX".
Copyrights notice
The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. Copyrights notice
Sistem serentak terdiri daripada pelbagai proses yang dijalankan secara serentak. Perintah pelaksanaan proses ini ditakrifkan oleh penjadual. Dalam teknik semakan model, dasar penjadualan berkait rapat dengan algoritma carian yang meneroka semua keadaan sistem. Untuk memastikan ketepatan sistem, dasar penjadualan perlu diambil kira semasa pengesahan. Pendekatan semasa, yang menggunakan strategi tetap, hanya mampu membuat jenis dasar yang terhad dan sukar untuk diperluaskan untuk mengendalikan variasi penjadual. Untuk menangani masalah ini, kami mencadangkan kaedah menggunakan bahasa khusus domain (DSL) untuk spesifikasi ringkas dasar penjadualan yang berbeza. Artifak yang diperlukan dijana secara automatik daripada spesifikasi untuk menganalisis gelagat sistem. Kami juga mencadangkan algoritma carian untuk meneroka ruang keadaan. Berdasarkan kaedah ini, kami membangunkan alat untuk mengesahkan sistem dengan penjadual. Percubaan kami menunjukkan bahawa kami boleh menyampaikan variasi penjadual dengan mudah dan mengesahkan sistem dengan tepat.
Nhat-Hoa TRAN
National University of Civil Engineering
Yuki CHIBA
DENSO CORPORATION
Toshiaki AOKI
Japan Advanced Institute of Science and Technology (JAIST)
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Salinan
Nhat-Hoa TRAN, Yuki CHIBA, Toshiaki AOKI, "Model Checking in the Presence of Schedulers Using a Domain-Specific Language for Scheduling Policies" in IEICE TRANSACTIONS on Information,
vol. E102-D, no. 7, pp. 1280-1295, July 2019, doi: 10.1587/transinf.2017EDP7391.
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2017EDP7391/_p
Salinan
@ARTICLE{e102-d_7_1280,
author={Nhat-Hoa TRAN, Yuki CHIBA, Toshiaki AOKI, },
journal={IEICE TRANSACTIONS on Information},
title={Model Checking in the Presence of Schedulers Using a Domain-Specific Language for Scheduling Policies},
year={2019},
volume={E102-D},
number={7},
pages={1280-1295},
abstract={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.},
keywords={},
doi={10.1587/transinf.2017EDP7391},
ISSN={1745-1361},
month={July},}
Salinan
TY - JOUR
TI - Model Checking in the Presence of Schedulers Using a Domain-Specific Language for Scheduling Policies
T2 - IEICE TRANSACTIONS on Information
SP - 1280
EP - 1295
AU - Nhat-Hoa TRAN
AU - Yuki CHIBA
AU - Toshiaki AOKI
PY - 2019
DO - 10.1587/transinf.2017EDP7391
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E102-D
IS - 7
JA - IEICE TRANSACTIONS on Information
Y1 - July 2019
AB - 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.
ER -