Garakabu2: An SMT-based Bounded Model Checker for HSTM Designs in ZIPC

Weiqiang Kong, Takahiro Ando, Hirokazu Yatsu, Kenji Hisazumi, Akira Fukuda

研究成果: Conference contribution

1 被引用数 (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 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 lebons on developing industry-oriented model checkers are also reported.

本文言語English
ホスト出版物のタイトルProceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015
出版社Institute of Electrical and Electronics Engineers Inc.
ページ21-29
ページ数9
ISBN(電子版)9781509002900
DOI
出版ステータスPublished - 2016 3月 15
外部発表はい
イベント2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015 - Wuhan, Hubei, China
継続期間: 2015 11月 162015 11月 19

出版物シリーズ

名前Proceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015

Conference

Conference2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015
国/地域China
CityWuhan, Hubei
Period15/11/1615/11/19

ASJC Scopus subject areas

  • コンピュータ ネットワークおよび通信
  • コンピュータ サイエンスの応用

フィンガープリント

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

引用スタイル