点击次数：

论文类型：期刊论文

发表时间：2016-12-01

发表刊物：JOURNAL OF INFORMATION SECURITY AND APPLICATIONS

收录刊物：Scopus、SCIE、EI

卷号：31

期号：,SI

页面范围：61-74

ISSN号：2214-2126

关键字：Satisfiability modulo theory; Bounded model check; ZIPC

摘要：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.