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

Research output: Contribution to journalArticle

10 Citations (Scopus)

Abstract

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.

Original languageEnglish
Pages (from-to)946-957
Number of pages12
JournalIEICE Transactions on Information and Systems
VolumeE94-D
Issue number5
DOIs
Publication statusPublished - May 2011

Fingerprint

Model checking
Industry
Experiments

All Science Journal Classification (ASJC) codes

  • Software
  • Hardware and Architecture
  • Computer Vision and Pattern Recognition
  • Electrical and Electronic Engineering
  • Artificial Intelligence

Cite this

An SMT-based approach to bounded model checking of designs in state transition matrix. / Kong, Weiqiang; Shiraishi, Tomohiro; Katahira, Noriyuki; Watanabe, Masahiko; Katayama, Tetsuro; Fukuda, Akira.

In: IEICE Transactions on Information and Systems, Vol. E94-D, No. 5, 05.2011, p. 946-957.

Research output: Contribution to journalArticle

Kong, Weiqiang ; Shiraishi, Tomohiro ; Katahira, Noriyuki ; Watanabe, Masahiko ; Katayama, Tetsuro ; Fukuda, Akira. / An SMT-based approach to bounded model checking of designs in state transition matrix. In: IEICE Transactions on Information and Systems. 2011 ; Vol. E94-D, No. 5. pp. 946-957.
@article{1640887327504c27a3c6e6a459840277,
title = "An SMT-based approach to bounded model checking of designs in state transition matrix",
abstract = "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.",
author = "Weiqiang Kong and Tomohiro Shiraishi and Noriyuki Katahira and Masahiko Watanabe and Tetsuro Katayama and Akira Fukuda",
year = "2011",
month = "5",
doi = "10.1587/transinf.E94.D.946",
language = "English",
volume = "E94-D",
pages = "946--957",
journal = "IEICE Transactions on Information and Systems",
issn = "0916-8532",
publisher = "一般社団法人電子情報通信学会",
number = "5",

}

TY - JOUR

T1 - An SMT-based approach to bounded model checking of designs in state transition matrix

AU - Kong, Weiqiang

AU - Shiraishi, Tomohiro

AU - Katahira, Noriyuki

AU - Watanabe, Masahiko

AU - Katayama, Tetsuro

AU - Fukuda, Akira

PY - 2011/5

Y1 - 2011/5

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=79955595443&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=79955595443&partnerID=8YFLogxK

U2 - 10.1587/transinf.E94.D.946

DO - 10.1587/transinf.E94.D.946

M3 - Article

AN - SCOPUS:79955595443

VL - E94-D

SP - 946

EP - 957

JO - IEICE Transactions on Information and Systems

JF - IEICE Transactions on Information and Systems

SN - 0916-8532

IS - 5

ER -