Garakabu2: An SMT-based Bounded Model Checker for HSTM Designs in ZIPC

Weiqiang Kong, Takahiro Ando, Hirokazu Yatsu, Hisazumi Kenji, Akira Fukuda

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

1 Citation (Scopus)

Abstract

Hierarchical State Transition Matrix (HSTM) is a table-based modeling language that has been broadly used for developing software designs of embedded systems. In this paper, we describe a model checker Garakabu2, which we have been implementing for verifying HSTM designs against LTL properties. The HSTM designs that Garakabu2 takes as input are those developed using an industrial-strength model-based development tool ZIPC. We focus on describing Garakabu2's verification techniques and performance as well as our effort to improve its practical usability for on-site software engineers. Some experience and lebons on developing industry-oriented model checkers are also reported.

Original languageEnglish
Title of host publicationProceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages21-29
Number of pages9
ISBN (Electronic)9781509002900
DOIs
Publication statusPublished - Mar 15 2016
Event2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015 - Wuhan, Hubei, China
Duration: Nov 16 2015Nov 19 2015

Publication series

NameProceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015

Other

Other2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015
CountryChina
CityWuhan, Hubei
Period11/16/1511/19/15

Fingerprint

Surface mount technology
Software design
Embedded systems
Engineers
Industry

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Computer Science Applications

Cite this

Kong, W., Ando, T., Yatsu, H., Kenji, H., & Fukuda, A. (2016). Garakabu2: An SMT-based Bounded Model Checker for HSTM Designs in ZIPC. In Proceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015 (pp. 21-29). [7434466] (Proceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/DCIT.2015.8

Garakabu2 : An SMT-based Bounded Model Checker for HSTM Designs in ZIPC. / Kong, Weiqiang; Ando, Takahiro; Yatsu, Hirokazu; Kenji, Hisazumi; Fukuda, Akira.

Proceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015. Institute of Electrical and Electronics Engineers Inc., 2016. p. 21-29 7434466 (Proceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015).

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

Kong, W, Ando, T, Yatsu, H, Kenji, H & Fukuda, A 2016, Garakabu2: An SMT-based Bounded Model Checker for HSTM Designs in ZIPC. in Proceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015., 7434466, Proceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015, Institute of Electrical and Electronics Engineers Inc., pp. 21-29, 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015, Wuhan, Hubei, China, 11/16/15. https://doi.org/10.1109/DCIT.2015.8
Kong W, Ando T, Yatsu H, Kenji H, Fukuda A. Garakabu2: An SMT-based Bounded Model Checker for HSTM Designs in ZIPC. In Proceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015. Institute of Electrical and Electronics Engineers Inc. 2016. p. 21-29. 7434466. (Proceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015). https://doi.org/10.1109/DCIT.2015.8
Kong, Weiqiang ; Ando, Takahiro ; Yatsu, Hirokazu ; Kenji, Hisazumi ; Fukuda, Akira. / Garakabu2 : An SMT-based Bounded Model Checker for HSTM Designs in ZIPC. Proceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015. Institute of Electrical and Electronics Engineers Inc., 2016. pp. 21-29 (Proceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015).
@inproceedings{e23efc53ceb34904a6cdd71b67e336d8,
title = "Garakabu2: An SMT-based Bounded Model Checker for HSTM Designs in ZIPC",
abstract = "Hierarchical State Transition Matrix (HSTM) is a table-based modeling language that has been broadly used for developing software designs of embedded systems. In this paper, we describe a model checker Garakabu2, which we have been implementing for verifying HSTM designs against LTL properties. The HSTM designs that Garakabu2 takes as input are those developed using an industrial-strength model-based development tool ZIPC. We focus on describing Garakabu2's verification techniques and performance as well as our effort to improve its practical usability for on-site software engineers. Some experience and lebons on developing industry-oriented model checkers are also reported.",
author = "Weiqiang Kong and Takahiro Ando and Hirokazu Yatsu and Hisazumi Kenji and Akira Fukuda",
year = "2016",
month = "3",
day = "15",
doi = "10.1109/DCIT.2015.8",
language = "English",
series = "Proceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "21--29",
booktitle = "Proceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015",
address = "United States",

}

TY - GEN

T1 - Garakabu2

T2 - An SMT-based Bounded Model Checker for HSTM Designs in ZIPC

AU - Kong, Weiqiang

AU - Ando, Takahiro

AU - Yatsu, Hirokazu

AU - Kenji, Hisazumi

AU - Fukuda, Akira

PY - 2016/3/15

Y1 - 2016/3/15

N2 - Hierarchical State Transition Matrix (HSTM) is a table-based modeling language that has been broadly used for developing software designs of embedded systems. In this paper, we describe a model checker Garakabu2, which we have been implementing for verifying HSTM designs against LTL properties. The HSTM designs that Garakabu2 takes as input are those developed using an industrial-strength model-based development tool ZIPC. We focus on describing Garakabu2's verification techniques and performance as well as our effort to improve its practical usability for on-site software engineers. Some experience and lebons on developing industry-oriented model checkers are also reported.

AB - Hierarchical State Transition Matrix (HSTM) is a table-based modeling language that has been broadly used for developing software designs of embedded systems. In this paper, we describe a model checker Garakabu2, which we have been implementing for verifying HSTM designs against LTL properties. The HSTM designs that Garakabu2 takes as input are those developed using an industrial-strength model-based development tool ZIPC. We focus on describing Garakabu2's verification techniques and performance as well as our effort to improve its practical usability for on-site software engineers. Some experience and lebons on developing industry-oriented model checkers are also reported.

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

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

U2 - 10.1109/DCIT.2015.8

DO - 10.1109/DCIT.2015.8

M3 - Conference contribution

AN - SCOPUS:84966553319

T3 - Proceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015

SP - 21

EP - 29

BT - Proceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015

PB - Institute of Electrical and Electronics Engineers Inc.

ER -