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

10 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

Model checking
Software design
Computer systems
Formal verification
Industry
Experiments

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

Formal verification of software designs in Hierarchical State Transition Matrix with SMT-based bounded model checking. / Kong, Weiqiang; Katahira, Noriyuki; Watanabe, Masahiko; Katayama, Tetsuro; Kenji, Hisazumi; Fukuda, Akira.

Proceedings - 18th Asia-Pacific Software Engineering Conference, APSEC 2011. 2011. p. 81-88 6130673.

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

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., 6130673, pp. 81-88, 18th Asia Pacific Software Engineering Conference, APSEC 2011, Ho Chi Minh, Viet Nam, 12/5/11. https://doi.org/10.1109/APSEC.2011.17
Kong W, Katahira N, Watanabe M, Katayama T, Kenji H, Fukuda A. 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. 2011. p. 81-88. 6130673 https://doi.org/10.1109/APSEC.2011.17
Kong, Weiqiang ; Katahira, Noriyuki ; Watanabe, Masahiko ; Katayama, Tetsuro ; Kenji, Hisazumi ; Fukuda, Akira. / 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. 2011. pp. 81-88
@inproceedings{22473d5f7e814f69bbd33abd454ec197,
title = "Formal verification of software designs in Hierarchical State Transition Matrix with SMT-based bounded model checking",
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.",
author = "Weiqiang Kong and Noriyuki Katahira and Masahiko Watanabe and Tetsuro Katayama and Hisazumi Kenji and Akira Fukuda",
year = "2011",
month = "12",
day = "1",
doi = "10.1109/APSEC.2011.17",
language = "English",
isbn = "9780769546094",
pages = "81--88",
booktitle = "Proceedings - 18th Asia-Pacific Software Engineering Conference, APSEC 2011",

}

TY - GEN

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

AU - Kong, Weiqiang

AU - Katahira, Noriyuki

AU - Watanabe, Masahiko

AU - Katayama, Tetsuro

AU - Kenji, Hisazumi

AU - Fukuda, Akira

PY - 2011/12/1

Y1 - 2011/12/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84856608577&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84856608577&partnerID=8YFLogxK

U2 - 10.1109/APSEC.2011.17

DO - 10.1109/APSEC.2011.17

M3 - Conference contribution

SN - 9780769546094

SP - 81

EP - 88

BT - Proceedings - 18th Asia-Pacific Software Engineering Conference, APSEC 2011

ER -