文献

J-GLOBAL ID：201202235405942938   整理番号：12A0385283

SMTソルバーを用いたUML状態機械の有界モデル検査に関する一考察

A Study for Bounded Model Checking of UML State Machines Using SMT Solvers

著者 (2件)： 新村勇人 (大阪大 大学院工学研究科) ,  宮本俊幸 (大阪大 大学院工学研究科)
資料名： 電子情報通信学会技術研究報告  (IEICE Technical Report (Institute of Electronics, Information and Communication Engineers))
巻： 111  号： 405(MSS2011 54-71)  ページ： 21-26  発行年： 2012年01月19日 
JST資料番号： S0532B  ISSN： 0913-5685  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 近年,記号モデル検査の有効な手法として命題論理式の充足可能性問題(satisfiability,SAT)を利用する有界モデル検査が注目を集めている。データを含む分散システムの有界モデル検査手法において,SATソルバーではなくSMTソルバー(SAT modulo theories)を用いるとより効率的であることが知られている。また,我々はSOAに基づくシステムを設計・検証するためのUMLサブセットとして,cbUMLを提案した。よって本論文では,cbUMLにおける状態機械のSMTソルバーを用いる有界モデル検査手法を考察する。(著者抄録)

シソーラス用語： *充足可能性問題 ,  応用プログラム ,  *UML【モデリング言語】 ,  *有限状態機械 ,  *モデル検査 ,  命題論理 ,  計算機システム ,  システムアーキテクチャ ,  システム設計 ,  検証 ,  状態遷移図 ,  通信方式 ,  表現
準シソーラス用語： サービス指向アーキテクチャ ,  システム検証 ,  ソルバ ,  記号表現 ,  非同期通信 ,  分散システム

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

タイトルに関連する用語 (5件)： SMT ,  ソルバー ,  UML ,  有界 ,  モデル検査