文献

J-GLOBAL ID：201902254142448296   整理番号：19A2422954

形式的方法によるより良い設計デバッグのための効果的誘導ヒントの同定【JST・京大機械翻訳】

Identification of Effective Guidance Hints for Better Design Debugging by Formal Methods

著者 (3件)： Vineesh V. S. (Computer Architecture and Dependable Systems Lab (CADSL), Department of Electrical Engineering, IIT Bombay, Mumbai, India) ,  Kumar Binod (Computer Architecture and Dependable Systems Lab (CADSL), Department of Electrical Engineering, IIT Bombay, Mumbai, India) ,  Adhaduk Jay (Computer Architecture and Dependable Systems Lab (CADSL), Department of Electrical Engineering, IIT Bombay, Mumbai, India)
資料名： Communications in Computer and Information Science  (Communications in Computer and Information Science)
巻： 1066  ページ： 413-427  発行年： 2019年 
JST資料番号： W5071A  ISSN： 1865-0929  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 形式的方法による完全な設計検証を達成することは,今日までの目標となっている。モデルチェッカーと他の形式的技術の進歩により,大規模設計は部分的または半形式的方法で検証できる。しかし,設計状態空間の徹底的な調査がまだ禁止されていることはよく知られている。本論文では,完全形式検証の有望性を保持するガイド状態空間探索の概念を再検討した。自動的な方法で誘導戦略を考案することは自明ではないので,誘導ヒントの同定は状態空間の方向横断に対して非常に重要になる。この指向トラバースは,最終的に形式的検証に費やされる時間を減少させることができ,また,より良い設計デバッギングを支援することができる。本論文では,このようなガイドポストの同定法を提案し,それらをデバッギング目的に利用した。著者らの目標は,ガイドポストの使用によるより速い対抗例生成を達成することである。複雑な設計に関する実験は,提案方法論によって同定された誘導ヒントが,異なる誤差トレースのためのモデル検査の間,有意な利得を提供することを示した。Copyright 2019 Springer Nature Singapore Pte Ltd. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 利得 ,  *デバッギング ,  モデル ,  モデル検査
準シソーラス用語： 形式的検証 ,  状態空間 ,  設計検証 , 【Automatic Indexing@JST】

著者キーワード (3件)： 形式的検証 ,  モデル検査 ,  時間論理

分類 (1件)： 計算機システム開発  (JD02010R)

タイトルに関連する用語 (6件)： 形式的方法 ,  設計 ,  デバッグ ,  誘導 ,  ヒント ,  同定