@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 Kenji Hisazumi and Akira Fukuda",
year = "2016",
month = mar,
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",
note = "2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015 ; Conference date: 16-11-2015 Through 19-11-2015",
}