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

Weiqiang Kong, Noriyuki Katahira, Wanpeng Qian, Masahiko Watanabe, Tetsuro Katayama, Akira Fukuda

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

5 被引用数 (Scopus)

抄録

State Transition Matrix (STM) is a table-based modeling language for developing designs of software systems. Although widely accepted and used in software industry, there is lack of formal verification supports for conducting rigorous analysis to improve reliability of STM designs. In this paper, we present a symbolic encoding approach for STM designs that employ message passing as the means of communication, through which correctness of a STM design with respect to invariant properties could be Bounded Model Checked (BMC) by using Satisfiability Modulo Theories (SMT) solving techniques. We have built a prototype implementation of the proposed encoding and the state-of-the-art SMT solver - Yices, is used in our experiments as a back-end tool to evaluate the effectiveness of our approach. In addition, two approaches for accelerating SMT solving by introducing additional knowledge are proposed and their effectiveness is shown by our preliminary experimental results.

本文言語英語
ホスト出版物のタイトルProceedings - 2011 International Conference on Computational Science and Its Applications, ICCSA 2011
ページ159-167
ページ数9
DOI
出版ステータス出版済み - 9 5 2011
イベント11th International Conference on Computational Science and Its Applications, ICCSA 2011 - Santander, スペイン
継続期間: 6 20 20116 23 2011

出版物シリーズ

名前Proceedings - 2011 International Conference on Computational Science and Its Applications, ICCSA 2011

その他

その他11th International Conference on Computational Science and Its Applications, ICCSA 2011
国/地域スペイン
CitySantander
Period6/20/116/23/11

All Science Journal Classification (ASJC) codes

  • 計算理論と計算数学
  • コンピュータ サイエンスの応用

フィンガープリント

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

引用スタイル