|
个人信息Personal Information
教授
博士生导师
硕士生导师
主要任职：软件学院、大连理工大学-立命馆大学国际信息与软件学院副院长
性别：男
毕业院校：北陆先端科学技术大学院大学
学位：博士
所在单位：软件学院、国际信息与软件学院
学科：软件工程
办公地点：综合楼525
联系方式：0411-62274401
电子邮箱：wqkong@dlut.edu.cn
Garakabu2: an SMT-based Bounded Model Checker for HSTM Designs in ZIPC
点击次数：
论文类型：会议论文
发表时间：2015-01-01
收录刊物：CPCI-S
页面范围：21-29
摘要：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 lessons on developing industry-oriented model checkers are also reported.