Release Time:2019-03-11  Hits:

Indexed by: Conference Paper

Date of Publication: 2015-01-01

Included Journals: CPCI-S

Page Number: 21-29

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 lessons on developing industry-oriented model checkers are also reported.