Hits:

Indexed by:会议论文

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.