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

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

研究成果: Article査読

8 被引用数 (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.

本文言語English
ページ(範囲)61-74
ページ数14
ジャーナルJournal of Information Security and Applications
31
DOI
出版ステータスPublished - 2016 12月 1
外部発表はい

ASJC Scopus subject areas

  • ソフトウェア
  • 安全性、リスク、信頼性、品質管理
  • コンピュータ ネットワークおよび通信

フィンガープリント

「Garakabu2: an SMT-based bounded model checker for HSTM designs in ZIPC」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル