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

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

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 lebons on developing industry-oriented model checkers are also reported.

Original languageEnglish
Title of host publicationProceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages21-29
Number of pages9
ISBN (Electronic)9781509002900
DOIs
Publication statusPublished - 2016 Mar 15
Externally publishedYes
Event2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015 - Wuhan, Hubei, China
Duration: 2015 Nov 162015 Nov 19

Publication series

NameProceedings - 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
Country/TerritoryChina
CityWuhan, Hubei
Period15/11/1615/11/19

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Computer Science Applications

Fingerprint

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