Garakabu2

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

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

Research output: Contribution to journalArticle

3 Citations (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 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
Volume31
DOIs
Publication statusPublished - Dec 1 2016

Fingerprint

Surface mount technology
Temporal logic
Software design
Embedded systems
Engineers
Industry

All Science Journal Classification (ASJC) codes

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

Cite this

Garakabu2 : an SMT-based bounded model checker for HSTM designs in ZIPC. / Kong, Weiqiang; Hou, Gang; Hu, Xiangpei; Ando, Takahiro; Kenji, Hisazumi; Fukuda, Akira.

In: Journal of Information Security and Applications, Vol. 31, 01.12.2016, p. 61-74.

Research output: Contribution to journalArticle

@article{b558458ad203403087e78dc1d026bdc2,
title = "Garakabu2: an SMT-based bounded model checker for HSTM designs in ZIPC",
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 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.",
author = "Weiqiang Kong and Gang Hou and Xiangpei Hu and Takahiro Ando and Hisazumi Kenji and Akira Fukuda",
year = "2016",
month = "12",
day = "1",
doi = "10.1016/j.jisa.2016.08.001",
language = "English",
volume = "31",
pages = "61--74",
journal = "Journal of Information Security and Applications",
issn = "2214-2126",
publisher = "Elsevier Limited",

}

TY - JOUR

T1 - Garakabu2

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

AU - Kong, Weiqiang

AU - Hou, Gang

AU - Hu, Xiangpei

AU - Ando, Takahiro

AU - Kenji, Hisazumi

AU - Fukuda, Akira

PY - 2016/12/1

Y1 - 2016/12/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84994121206&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84994121206&partnerID=8YFLogxK

U2 - 10.1016/j.jisa.2016.08.001

DO - 10.1016/j.jisa.2016.08.001

M3 - Article

VL - 31

SP - 61

EP - 74

JO - Journal of Information Security and Applications

JF - Journal of Information Security and Applications

SN - 2214-2126

ER -