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

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

11 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationProceedings - 18th Asia-Pacific Software Engineering Conference, APSEC 2011
Pages81-88
Number of pages8
DOIs
Publication statusPublished - Dec 1 2011
Event18th Asia Pacific Software Engineering Conference, APSEC 2011 - Ho Chi Minh, Viet Nam
Duration: Dec 5 2011Dec 8 2011

Other

Other18th Asia Pacific Software Engineering Conference, APSEC 2011
CountryViet Nam
CityHo Chi Minh
Period12/5/1112/8/11

    Fingerprint

All Science Journal Classification (ASJC) codes

  • Software

Cite this

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