Garakabu2: an SMT-based bounded model checker for HSTM designs in ZIPC

Weiqiang Kong, Gang Hou, Xiangpei Hu, Takahiro Ando, Kenji Hisazumi, Akira Fukuda

Research output: Contribution to journalArticlepeer-review

9 Citations (Scopus)


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.

Original languageEnglish
Pages (from-to)61-74
Number of pages14
JournalJournal of Information Security and Applications
Publication statusPublished - Dec 1 2016

All Science Journal Classification (ASJC) codes

  • Software
  • Safety, Risk, Reliability and Quality
  • Computer Networks and Communications


Dive into the research topics of 'Garakabu2: an SMT-based bounded model checker for HSTM designs in ZIPC'. Together they form a unique fingerprint.

Cite this