Interval-based Counterexample Analysis for Error Explanation

• Item type: Journal(1)
• 公開日: 2021-10-15
• タイトル: Interval-based Counterexample Analysis for Error Explanation
• タイトル / 言語: en
• タイトル: Interval-based Counterexample Analysis for Error Explanation
• 言語: eng
• キーワード / 主題Scheme: Other
• キーワード / 主題: [一般論文] bounded model checking, AllSAT solver, BDD, network verification, counterexample, error explanation
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: Graduate School of Informatics and Engineering, the University of Electro-Communications
• 著者所属: NTT Network Innovation Laboratories, NTT Corporation
• 著者所属(英): en
• 著者所属(英): Graduate School of Informatics and Engineering, the University of Electro-Communications
• 著者所属(英): en
• 著者所属(英): NTT Network Innovation Laboratories, NTT Corporation
• 著者名: Takahisa, Toda; Takeru, Inoue
• 著者名(英): Takahisa, Toda; Takeru, Inoue
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: Model checking is an automated reasoning technique for the verification of hardware and software. If there is a fault in a system description, model checkers return, as an explanation of failure, a single execution trace of the system that results in an error state. Counterexamples are useful clues for locating faults, however, there is a big gap between computing counterexamples and locating faults, and the fault localization task is done by a manual inspection of counterexamples, which largely depends on individual expertise and intuition. Effective explanation of the failure is, thus, considered as an important issue. Since a single counterexample returned by model checkers is only one instance of failing executions, it is hard to gain clear perspective on the failure with just one specific case. In this paper we take another approach for error explanation: we generate many counterexamples and then abstract an essence of the failure from them. For example, in the formal verification of network configuration, a range of possible values (naturally identified with integers) to a single variable often makes it easier to understand the essence of the failure. In our experiments, such a range of values (called interval) is simply a set of consecutive IP addresses and can be substantially represented in two end addresses. We formulate the notion of intervals in a general setting. The concept of intervals is not limited to network configuration and it can be considered in an arbitrary system model as long as a variable on which interval is computed substantially takes integers. We present a method for computing the longest interval by combining bounded model checking, BDD, and AllSAT solver. To evaluate our method for the longest interval computation, we conduct experiments with a real network dataset and its randomly modified dataset. We confirm that about 8 millions of counterexamples are generated in 1.61s and among them, the longest interval of length about 600 millions is reported in less than 0.01s.; ------------------------------; This is a preprint of an article intended for publication Journal of; Information Processing(JIP). This preprint should not be cited. This; article should be cited as: Journal of Information Processing Vol.29(2021) (online); DOI http://dx.doi.org/10.2197/ipsjjip.29.630; ------------------------------
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Model checking is an automated reasoning technique for the verification of hardware and software. If there is a fault in a system description, model checkers return, as an explanation of failure, a single execution trace of the system that results in an error state. Counterexamples are useful clues for locating faults, however, there is a big gap between computing counterexamples and locating faults, and the fault localization task is done by a manual inspection of counterexamples, which largely depends on individual expertise and intuition. Effective explanation of the failure is, thus, considered as an important issue. Since a single counterexample returned by model checkers is only one instance of failing executions, it is hard to gain clear perspective on the failure with just one specific case. In this paper we take another approach for error explanation: we generate many counterexamples and then abstract an essence of the failure from them. For example, in the formal verification of network configuration, a range of possible values (naturally identified with integers) to a single variable often makes it easier to understand the essence of the failure. In our experiments, such a range of values (called interval) is simply a set of consecutive IP addresses and can be substantially represented in two end addresses. We formulate the notion of intervals in a general setting. The concept of intervals is not limited to network configuration and it can be considered in an arbitrary system model as long as a variable on which interval is computed substantially takes integers. We present a method for computing the longest interval by combining bounded model checking, BDD, and AllSAT solver. To evaluate our method for the longest interval computation, we conduct experiments with a real network dataset and its randomly modified dataset. We confirm that about 8 millions of counterexamples are generated in 1.61s and among them, the longest interval of length about 600 millions is reported in less than 0.01s.; ------------------------------; This is a preprint of an article intended for publication Journal of; Information Processing(JIP). This preprint should not be cited. This; article should be cited as: Journal of Information Processing Vol.29(2021) (online); DOI http://dx.doi.org/10.2197/ipsjjip.29.630; ------------------------------
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00116647
• 書誌情報: 情報処理学会論文誌; 巻 62, 号 10, 発行日 2021-10-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7764