文献

J-GLOBAL ID：201002245781269528   整理番号：10A0057009

最近のSAT技術の発展 SATによるシステム検証

著者 (2件)： 番原睦則 (神戸大 学術情報基盤セ) ,  田村直之 (神戸大 学術情報基盤セ)
資料名： 人工知能学会誌  (Journal of the Japanese Society for Artificial Intelligence)
巻： 25  号： 1  ページ： 122-129  発行年： 2010年01月01日 
JST資料番号： X0330A  ISSN： 0912-8085  資料種別： 逐次刊行物 (A)
記事区分： 解説  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 命題論理の充足可能性判定(SAT)問題を解くSATソルバーが飛躍的に向上し,ハードウェア・ソフトウェアの信頼性を高めるためのシステム検証への応用が試みられている。本論文では,SAT技術を用いたモデル検査手法の1つである有界モデル検査(BMC),及びソフトウェア・ハードウェアのテスト手法の1つである組合せテストについて述べた。BMCは与えられた安全性や活性を表すLTL(Linear Temporal Logic)の論理式から性質の否定命題を構成し,連言標準形に変換してSATソルバーに入力して性質の反例を探す不完全な手続きである。そこで,性質の証明を得る方法として帰納法を用いる方法を説明した。また,組合せテスト手法としてはk個の2値入力を持つ回路において任意のt(t<k)個の入力に対し,必要となるテストケース数の最小値を求める被覆配列の構成問題を解説した。前記問題は制約充足問題として定式化できるのでSAT符号化を用い,SATを用いたテストケース自動生成に関する実験結果を紹介した。

シソーラス用語： *充足可能性問題 ,  命題論理 ,  *モデル検査 ,  時間論理 ,  定理証明 ,  配列 ,  *最小化問題 ,  生産
準シソーラス用語： SATソルバ ,  SAT符号化 ,  テストケース ,  帰納法 ,  自動生成 ,  線形時間論理 ,  被覆配列 ,  *有界モデル検査

分類 (3件)： 論理代数  (JB03000H) ,  計算理論  (JB02000A) ,  その他のオペレーションズリサーチの手法  (KA03070E)

引用文献 (31件)：

• BIERE, A. Symbolic model checking without BDDs. Proc. 5th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99). 1999, 193-207
• BIERE, A. Bounded Model Checking. Handbook of Satisfiability. 2009, 457-481
• CHATEAUNEUF, M. A. On the state of strength-three covering arrays. J. Combinatorial Designs. 2002, 10, 4, 217-238
• CLARKE, E. M. Design and synthesis of symchronization skeletons using branching-time temporal logic. Proc. Workshop on Logic Programs, 1982. 1982
• CLARKE, E. M. Model Checking. 1999

タイトルに関連する用語 (3件)： SAT ,  発展 ,  システム検証