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

研究成果: Chapter in Book/Report/Conference proceedingConference 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.

元の言語英語
ホスト出版物のタイトルProceedings - 18th Asia-Pacific Software Engineering Conference, APSEC 2011
ページ81-88
ページ数8
DOI
出版物ステータス出版済み - 12 1 2011
イベント18th Asia Pacific Software Engineering Conference, APSEC 2011 - Ho Chi Minh, ベトナム
継続期間: 12 5 201112 8 2011

その他

その他18th Asia Pacific Software Engineering Conference, APSEC 2011
ベトナム
Ho Chi Minh
期間12/5/1112/8/11

All Science Journal Classification (ASJC) codes

  • Software

フィンガープリント Formal verification of software designs in Hierarchical State Transition Matrix with SMT-based bounded model checking' の研究トピックを掘り下げます。これらはともに一意のフィンガープリントを構成します。

  • これを引用

    Kong, W., Katahira, N., Watanabe, M., Katayama, T., Hisazumi, K., & Fukuda, A. (2011). Formal verification of software designs in Hierarchical State Transition Matrix with SMT-based bounded model checking. : Proceedings - 18th Asia-Pacific Software Engineering Conference, APSEC 2011 (pp. 81-88). [6130673] https://doi.org/10.1109/APSEC.2011.17