TY - GEN
T1 - Garakabu2
T2 - 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015
AU - Kong, Weiqiang
AU - Ando, Takahiro
AU - Yatsu, Hirokazu
AU - Hisazumi, Kenji
AU - Fukuda, Akira
N1 - Funding Information:
This research is supported by National Natural Science Foundation of China (Grant No. 61572097 , 61402073 , 71531002 ) and the Fundamental Research Funds for the Central University , China (Grant No. DUT14RC(3)150 ).
Publisher Copyright:
© 2015 IEEE.
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.
Y2 - 16 November 2015 through 19 November 2015
ER -