An SMT approach to bounded model checking of design in state transition matrix

Weiqiang Kong, Tomohiro Shiraishi, Yuki Mizushima, Noriyuki Katahira, Akira Fukuda, Masahiko Watanabe

研究成果: Chapter in Book/Report/Conference proceedingConference contribution

2 被引用数 (Scopus)

抄録

State Transition Matrix (STM) is a table-based modeling language that has been frequently used in industry for specifying behavior of distributed systems. Functional correctness of a STM design (i.e., a design written in STM) could usually be expressed as invariant properties. In this paper, we first present a formalization of the static and dynamic aspects of a STM design. Consequentially, based on this formalization, we investigate a symbolic encoding approach for STM design, through which the design could be bounded model checked wrt. 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.

本文言語英語
ホスト出版物のタイトルProceedings - 2010 10th International Conference on Computational Science and Its Applications, ICCSA 2010
編集者Andres Iglesias, Osvaldo Gervasi, Marina L. Gavrilova, David Taniar, Bernady O. Apduhan
出版社Institute of Electrical and Electronics Engineers Inc.
ページ231-238
ページ数8
ISBN(電子版)9780769539997
DOI
出版ステータス出版済み - 1 1 2010
イベント10th International Conference on Computational Science and Its Applications, ICCSA 2010 - Fukuoka, 日本
継続期間: 3 23 20103 26 2010

出版物シリーズ

名前Proceedings - 2010 10th International Conference on Computational Science and Its Applications, ICCSA 2010

その他

その他10th International Conference on Computational Science and Its Applications, ICCSA 2010
国/地域日本
CityFukuoka
Period3/23/103/26/10

All Science Journal Classification (ASJC) codes

  • 人工知能
  • コンピュータ ネットワークおよび通信
  • コンピュータ サイエンスの応用
  • 信号処理
  • 計算力学
  • 計算数学
  • 数値解析

フィンガープリント

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

引用スタイル