For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
An SMT-Based Approach to Bounded Model Checking of Designs in State Transition Matrix
Weiqiang KONG Tomohiro SHIRAISHI Noriyuki KATAHIRA Masahiko WATANABE Tetsuro KATAYAMA Akira FUKUDA
IEICE TRANSACTIONS on Information and Systems
Publication Date: 2011/05/01
Online ISSN: 1745-1361
Print ISSN: 0916-8532
Type of Manuscript: Special Section PAPER (Special Section on Formal Approach)
Category: Model Checking
state transition matrix, bounded model checking, invariant properties, satisfiability modulo theories,
Full Text: PDF(433.7KB)>>
State Transition Matrix (STM) is a table-based modeling language that has been frequently used in industry for specifying behaviors of systems. Functional correctness of a STM design (i.e., a design developed with STM) could often be expressed as invariant properties. In this paper, we first present a formalization of the static and dynamic aspects of STM designs. Consequentially, based on this formalization, we investigate a symbolic encoding approach, through which a STM design could be bounded model checked w.r.t. invariant properties by using Satisfiability Modulo Theories (SMT) solving technique. We have built a prototype implementation of the proposed encoding and the state-of-the-art SMT solver - Yices, is used in our experiments to evaluate the effectiveness of our approach. Two attempts for accelerating SMT solving are also reported.