On accelerating SMT-based bounded model checking of HSTM designs

Weiqiang Kong, Leyuan Liu, Yoriyuki Yamagata, Kenji Taguchi, Hitoshi Ohsaki, Akira Fukuda

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

6 被引用数 (Scopus)

抄録

Hierarchical State Transition Matrix (HSTM) is a table-based modeling language for developing designs of software systems. We have proposed a Satisfiability Modulo Theory (SMT) based Bounded Model Checking (BMC) approach in [1] to provide formal verification supports for conducting rigorous and automatic analysis to improve reliability of HSTM designs. In this paper, we continue that work by developing and evaluating approaches to accelerating BMC of HSTM designs. The approaches center around an unrolled Bounded Reach ability Tree (BRT) of a HSTM design that is built with stateless explicit state exploration. Specifically, reach ability of invalid cells (representing undesired states) of a HSTM design, which occurs within the bound concerned, could be discovered during construction of the BRT, and furthermore, if no such occurrence, the constructed BRT could be utilized to rule out unnecessary subformulas of a BMC instance for verification of LTL properties. We have implemented these approaches in a tool called Garakabu2 with the state-of-the-art SMT solver CVC3 as its back-ended solver. Our preliminary experiments show that verification could be accelerated substantially.

本文言語英語
ホスト出版物のタイトルAPSEC 2012 - Proceedings of the 19th Asia-Pacific Software Engineering Conference
出版社IEEE Computer Society
ページ614-623
ページ数10
ISBN(印刷版)9780769549224
DOI
出版ステータス出版済み - 2012
イベント19th Asia-Pacific Software Engineering Conference, APSEC 2012 - Hong Kong, 中国
継続期間: 12 4 201212 7 2012

出版物シリーズ

名前Proceedings - Asia-Pacific Software Engineering Conference, APSEC
1
ISSN(印刷版)1530-1362

その他

その他19th Asia-Pacific Software Engineering Conference, APSEC 2012
Country中国
CityHong Kong
Period12/4/1212/7/12

All Science Journal Classification (ASJC) codes

  • Software

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

引用スタイル