文献

J-GLOBAL ID：201702213216753943   整理番号：17A1774656

シータ:抽象化精密化ベースモデル検査のためのフレームワーク【Powered by NICT】

Theta: A framework for abstraction refinement-based model checking

著者 (5件)： Toth Tamas (Budapest University of Technology and Economics, Department of Measurement and Information Systems) ,  Hajdu Akos (Budapest University of Technology and Economics, Department of Measurement and Information Systems) ,  Vorcos Andras (Budapest University of Technology and Economics, Department of Measurement and Information Systems) ,  Micskei Zoltan (Budapest University of Technology and Economics, Department of Measurement and Information Systems) ,  Majzik Istvan (Budapest University of Technology and Economics, Department of Measurement and Information Systems)
資料名： IEEE Conference Proceedings  (IEEE Conference Proceedings)
巻： 2017  号： FMCAD  ページ： 176-179  発行年： 2017年 
JST資料番号： W2441A  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 本論文では,シータ,構成可能モデル検査フレームワークを提案した。フレームワークの目的は,種々の形式のモデルのための設計,施工と抽象詳細化ベース可到達性解析アルゴリズムの評価を支援することである。抽象化および精密化のための入力形式,抽象ドメインモデルインタプリタ,と戦略の定義を可能にした。現在,遷移システム,制御フローオートマトンと時間付きオートマトンのためのフロントエンド支援を含んでいる。内蔵抽象ドメインは述語,明確な値,ゾーンおよびそれらの組合せを含む,実施されたいろいろな微細化戦略であった。フレームワークの構成可能性は,いくつかの抽象化と精密化法の統合を可能にし,この方法は,それらの利点と欠点の評価を支持した。PLC,ハードウェア,Cプログラムと時間付きオートマトンモデルの安全性照査のためのユースケースによって,本フレームワークの適用性を実証した。Copyright 2017 The Institute of Electrical and Electronics Engineers, Inc. All Rights reserved. Translated from English into Japanese by JST【Powered by NICT】

シソーラス用語： オートマトン ,  *モデル検査 ,  ハードウェア ,  安全性 ,  遷移システム ,  *精密化 ,  適応性
準シソーラス用語： ユースケース ,  述語 ,  内蔵 ,  時間付きオートマトン ,  制御フロー , 【Automatic Indexing@JST】

分類 (1件)： 計算理論  (JB02000A)

タイトルに関連する用語 (4件)： 抽象化 ,  精密化 ,  モデル検査 ,  フレームワーク