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 language | English |
|---|---|
| Title of host publication | 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 |
| Number of pages | 9 |
| ISBN (Electronic) | 9781509002900 |
| DOIs | |
| Publication status | Published - Mar 15 2016 |
| Event | 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015 - Wuhan, Hubei, China Duration: Nov 16 2015 → Nov 19 2015 |
Publication series
| Name | Proceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015 |
|---|
Other
| Other | 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015 |
|---|---|
| Country | China |
| City | Wuhan, Hubei |
| Period | 11/16/15 → 11/19/15 |
Fingerprint
All Science Journal Classification (ASJC) codes
- Computer Networks and Communications
- Computer Science Applications
Cite this
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 proceeding › Conference contribution
}
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 -