Release Time:2019-03-12  Hits:

Indexed by: Journal Article

Date of Publication: 2016-12-01

Journal: JOURNAL OF INFORMATION SECURITY AND APPLICATIONS

Included Journals: EI、SCIE、Scopus

Volume: 31

Issue: ,SI

Page Number: 61-74

ISSN: 2214-2126

Key Words: Satisfiability modulo theory; Bounded model check; 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. (C) 2016 Elsevier Ltd. All rights reserved.