Formal verification of software designs in Hierarchical State Transition Matrix with SMT-based bounded model checking

Weiqiang Kong, Noriyuki Katahira, Masahiko Watanabe, Tetsuro Katayama, Kenji Hisazumi, Akira Fukuda

研究成果: Conference contribution

12 被引用数 (Scopus)

抄録

Hierarchical State Transition Matrix (HSTM) is a table-based modeling language for developing designs of software systems. Although widely used and adopted by (particularly Japanese) software industry, there is still lack of mechanized formal verification supports for conducting rigorous and automatic analysis to improve reliability of HSTM designs. In this paper, we first present a formalization of HSTM designs as state transition systems. Consequentially, based on this formalization, we propose a symbolic encoding approach, through which correctness of a HSTM design with respect to LTL properties could be represented as Bounded Model Checking (BMC) problems that could be determined by Satisfiability Modulo Theories (SMT) solving. We have implemented our encoding approach in a tool called Garakabu2 with the state-of-the-art SMT solver CVC3 as its back-ended solver. Furthermore, in our preliminary experiments, a conceptually simple but steadily effective way of accelerating SMT solving for HSTM designs is investigated and reported.

本文言語English
ホスト出版物のタイトルProceedings - 18th Asia-Pacific Software Engineering Conference, APSEC 2011
ページ81-88
ページ数8
DOI
出版ステータスPublished - 2011
外部発表はい
イベント18th Asia Pacific Software Engineering Conference, APSEC 2011 - Ho Chi Minh, Viet Nam
継続期間: 2011 12 52011 12 8

出版物シリーズ

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

Conference

Conference18th Asia Pacific Software Engineering Conference, APSEC 2011
国/地域Viet Nam
CityHo Chi Minh
Period11/12/511/12/8

ASJC Scopus subject areas

  • ソフトウェア

フィンガープリント

「Formal verification of software designs in Hierarchical State Transition Matrix with SMT-based bounded model checking」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル