An SMT approach to bounded model checking of design in state transition matrix

Weiqiang Kong, Tomohiro Shiraishi, Yuki Mizushima, Noriyuki Katahira, Akira Fukuda, Masahiko Watanabe

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

State Transition Matrix (STM) is a table-based modeling language that has been frequently used in industry for specifying behavior of distributed systems. Functional correctness of a STM design (i.e., a design written in STM) could usually be expressed as invariant properties. In this paper, we first present a formalization of the static and dynamic aspects of a STM design. Consequentially, based on this formalization, we investigate a symbolic encoding approach for STM design, through which the design could be bounded model checked wrt. 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.

Original languageEnglish
Title of host publicationProceedings - 2010 10th International Conference on Computational Science and Its Applications, ICCSA 2010
EditorsAndres Iglesias, Osvaldo Gervasi, Marina L. Gavrilova, David Taniar, Bernady O. Apduhan
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages231-238
Number of pages8
ISBN (Electronic)9780769539997
DOIs
Publication statusPublished - Jan 1 2010
Event10th International Conference on Computational Science and Its Applications, ICCSA 2010 - Fukuoka, Japan
Duration: Mar 23 2010Mar 26 2010

Publication series

NameProceedings - 2010 10th International Conference on Computational Science and Its Applications, ICCSA 2010

Other

Other10th International Conference on Computational Science and Its Applications, ICCSA 2010
CountryJapan
CityFukuoka
Period3/23/103/26/10

All Science Journal Classification (ASJC) codes

  • Artificial Intelligence
  • Computer Networks and Communications
  • Computer Science Applications
  • Signal Processing
  • Computational Mechanics
  • Computational Mathematics
  • Numerical Analysis

Fingerprint Dive into the research topics of 'An SMT approach to bounded model checking of design in state transition matrix'. Together they form a unique fingerprint.

Cite this