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  

Publication
IEICE TRANSACTIONS on Information and Systems   Vol.E94-D   No.5   pp.946-957
Publication Date: 2011/05/01
Online ISSN: 1745-1361
DOI: 10.1587/transinf.E94.D.946
Print ISSN: 0916-8532
Type of Manuscript: Special Section PAPER (Special Section on Formal Approach)
Category: Model Checking
Keyword: 
state transition matrix,  bounded model checking,  invariant properties,  satisfiability modulo theories,  

Full Text: PDF(433.7KB)>>
Buy this Article




Summary: 
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.