On accelerating SMT-based bounded model checking of HSTM designs

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

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

6 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationAPSEC 2012 - Proceedings of the 19th Asia-Pacific Software Engineering Conference
PublisherIEEE Computer Society
Pages614-623
Number of pages10
Volume1
ISBN (Print)9780769549224
DOIs
Publication statusPublished - Jan 1 2012
Event19th Asia-Pacific Software Engineering Conference, APSEC 2012 - Hong Kong, China
Duration: Dec 4 2012Dec 7 2012

Other

Other19th Asia-Pacific Software Engineering Conference, APSEC 2012
CountryChina
CityHong Kong
Period12/4/1212/7/12

Fingerprint

Model checking
Computer systems
Experiments

All Science Journal Classification (ASJC) codes

  • Software

Cite this

Kong, W., Liu, L., Yamagata, Y., Taguchi, K., Ohsaki, H., & Fukuda, A. (2012). On accelerating SMT-based bounded model checking of HSTM designs. In APSEC 2012 - Proceedings of the 19th Asia-Pacific Software Engineering Conference (Vol. 1, pp. 614-623). [6462717] IEEE Computer Society. https://doi.org/10.1109/APSEC.2012.38

On accelerating SMT-based bounded model checking of HSTM designs. / Kong, Weiqiang; Liu, Leyuan; Yamagata, Yoriyuki; Taguchi, Kenji; Ohsaki, Hitoshi; Fukuda, Akira.

APSEC 2012 - Proceedings of the 19th Asia-Pacific Software Engineering Conference. Vol. 1 IEEE Computer Society, 2012. p. 614-623 6462717.

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

Kong, W, Liu, L, Yamagata, Y, Taguchi, K, Ohsaki, H & Fukuda, A 2012, On accelerating SMT-based bounded model checking of HSTM designs. in APSEC 2012 - Proceedings of the 19th Asia-Pacific Software Engineering Conference. vol. 1, 6462717, IEEE Computer Society, pp. 614-623, 19th Asia-Pacific Software Engineering Conference, APSEC 2012, Hong Kong, China, 12/4/12. https://doi.org/10.1109/APSEC.2012.38
Kong W, Liu L, Yamagata Y, Taguchi K, Ohsaki H, Fukuda A. On accelerating SMT-based bounded model checking of HSTM designs. In APSEC 2012 - Proceedings of the 19th Asia-Pacific Software Engineering Conference. Vol. 1. IEEE Computer Society. 2012. p. 614-623. 6462717 https://doi.org/10.1109/APSEC.2012.38
Kong, Weiqiang ; Liu, Leyuan ; Yamagata, Yoriyuki ; Taguchi, Kenji ; Ohsaki, Hitoshi ; Fukuda, Akira. / On accelerating SMT-based bounded model checking of HSTM designs. APSEC 2012 - Proceedings of the 19th Asia-Pacific Software Engineering Conference. Vol. 1 IEEE Computer Society, 2012. pp. 614-623
@inproceedings{b0490952131e43318d70a30435e47374,
title = "On accelerating SMT-based bounded model checking of HSTM designs",
abstract = "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.",
author = "Weiqiang Kong and Leyuan Liu and Yoriyuki Yamagata and Kenji Taguchi and Hitoshi Ohsaki and Akira Fukuda",
year = "2012",
month = "1",
day = "1",
doi = "10.1109/APSEC.2012.38",
language = "English",
isbn = "9780769549224",
volume = "1",
pages = "614--623",
booktitle = "APSEC 2012 - Proceedings of the 19th Asia-Pacific Software Engineering Conference",
publisher = "IEEE Computer Society",
address = "United States",

}

TY - GEN

T1 - On accelerating SMT-based bounded model checking of HSTM designs

AU - Kong, Weiqiang

AU - Liu, Leyuan

AU - Yamagata, Yoriyuki

AU - Taguchi, Kenji

AU - Ohsaki, Hitoshi

AU - Fukuda, Akira

PY - 2012/1/1

Y1 - 2012/1/1

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

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

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

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

U2 - 10.1109/APSEC.2012.38

DO - 10.1109/APSEC.2012.38

M3 - Conference contribution

AN - SCOPUS:84874583834

SN - 9780769549224

VL - 1

SP - 614

EP - 623

BT - APSEC 2012 - Proceedings of the 19th Asia-Pacific Software Engineering Conference

PB - IEEE Computer Society

ER -