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 Linear Temporal Logic (LTL) properties. The HSTM designs that Garakabu2 takes as input are those developed using an industrial-strength model-based development environment ZIPC. We focus on describing Garakabu2's verification techniques and performance, as well as our efforts to improve its practical usability for on-site software engineers. Some experiences and lessons on developing industry-oriented model checkers are also reported.
- Bounded model check
- Satisfiability modulo theory
ASJC Scopus subject areas
- Safety, Risk, Reliability and Quality
- Computer Networks and Communications