An SMT-based approach to bounded model checking of designs in state transition matrix

Weiqiang Kong, Tomohiro Shiraishi, Noriyuki Katahira, Masahiko Watanabe, Tetsuro Katayama, Akira Fukuda

研究成果: Contribution to journalArticle査読

10 被引用数 (Scopus)

抄録

State Transition Matrix (STM) is a table-based modeling language that has been frequently used in industry for specifying behaviors of systems. Functional correctness of a STM design (i.e., a design developed with STM) could often be expressed as invariant properties. In this paper, we first present a formalization of the static and dynamic aspects of STM designs. Consequentially, based on this formalization, we investigate a symbolic encoding approach, through which a STM design could be bounded model checked w.r.t. invariant properties by using Satisfiability Modulo Theories (SMT) solving technique. We have built a prototype implementation of the proposed encoding and the state-of-the-art SMT solver - Yices, is used in our experiments to evaluate the effectiveness of our approach. Two attempts for accelerating SMT solving are also reported.

本文言語英語
ページ(範囲)946-957
ページ数12
ジャーナルIEICE Transactions on Information and Systems
E94-D
5
DOI
出版ステータス出版済み - 5 2011

All Science Journal Classification (ASJC) codes

  • ソフトウェア
  • ハードウェアとアーキテクチャ
  • コンピュータ ビジョンおよびパターン認識
  • 電子工学および電気工学
  • 人工知能

フィンガープリント

「An SMT-based approach to bounded model checking of designs in state transition matrix」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル