{"metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00213305","sets":["581:10433:10443"]},"path":["10443"],"owner":"44499","recid":"213305","title":["Interval-based Counterexample Analysis for Error Explanation "],"pubdate":{"attribute_name":"公開日","attribute_value":"2021-10-15"},"_buckets":{"deposit":"20e6cfbb-867a-4359-93a7-22f8acc8c88b"},"_deposit":{"id":"213305","pid":{"type":"depid","value":"213305","revision_id":0},"owners":[44499],"status":"published","created_by":44499},"item_title":"Interval-based Counterexample Analysis for Error Explanation ","author_link":["545628","545629","545627","545630"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"Interval-based Counterexample Analysis for Error Explanation "},{"subitem_title":"Interval-based Counterexample Analysis for Error Explanation ","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"[一般論文] bounded model checking, AllSAT solver, BDD, network verification, counterexample, error explanation","subitem_subject_scheme":"Other"}]},"item_type_id":"2","publish_date":"2021-10-15","item_2_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"Graduate School of Informatics and Engineering, the University of Electro-Communications"},{"subitem_text_value":"NTT Network Innovation Laboratories, NTT Corporation"}]},"item_2_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Graduate School of Informatics and Engineering, the University of Electro-Communications","subitem_text_language":"en"},{"subitem_text_value":"NTT Network Innovation Laboratories, NTT Corporation","subitem_text_language":"en"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"eng"}]},"publish_status":"0","weko_shared_id":-1,"item_file_price":{"attribute_name":"Billing file","attribute_type":"file","attribute_value_mlt":[{"url":{"url":"https://ipsj.ixsq.nii.ac.jp/record/213305/files/IPSJ-JNL6210010.pdf","label":"IPSJ-JNL6210010.pdf"},"date":[{"dateType":"Available","dateValue":"2023-10-15"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-JNL6210010.pdf","filesize":[{"value":"530.9 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"0","billingrole":"5"},{"tax":["include_tax"],"price":"0","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"8"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"94c12ec6-8cba-4443-991f-4924121ee41a","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2021 by the Information Processing Society of Japan"}]},"item_2_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Takahisa, Toda"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Takeru, Inoue"}],"nameIdentifiers":[{}]}]},"item_2_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Takahisa, Toda","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Takeru, Inoue","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_2_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AN00116647","subitem_source_identifier_type":"NCID"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_6501","resourcetype":"journal article"}]},"item_2_source_id_11":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"1882-7764","subitem_source_identifier_type":"ISSN"}]},"item_2_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"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.\n------------------------------\nThis is a preprint of an article intended for publication Journal of\nInformation Processing(JIP). This preprint should not be cited. This\narticle should be cited as: Journal of Information Processing Vol.29(2021) (online)\nDOI　http://dx.doi.org/10.2197/ipsjjip.29.630\n------------------------------","subitem_description_type":"Other"}]},"item_2_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"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.\n------------------------------\nThis is a preprint of an article intended for publication Journal of\nInformation Processing(JIP). This preprint should not be cited. This\narticle should be cited as: Journal of Information Processing Vol.29(2021) (online)\nDOI　http://dx.doi.org/10.2197/ipsjjip.29.630\n------------------------------","subitem_description_type":"Other"}]},"item_2_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographic_titles":[{"bibliographic_title":"情報処理学会論文誌"}],"bibliographicIssueDates":{"bibliographicIssueDate":"2021-10-15","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"10","bibliographicVolumeNumber":"62"}]},"relation_version_is_last":true,"weko_creator_id":"44499"},"id":213305,"updated":"2025-01-19T17:12:24.850555+00:00","links":{},"created":"2025-01-19T01:14:11.330182+00:00"}