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

Fingerprint

Bounded Model Checking
Transition Matrix
Model checking
State Transition
Modulo
Formalization
Encoding
Invariant
Modeling Language
Distributed Systems
Correctness
Table
Design
Prototype
Industry
Evaluate
Experiment
Experiments

All Science Journal Classification (ASJC) codes

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

Cite this

Kong, W., Shiraishi, T., Mizushima, Y., Katahira, N., Fukuda, A., & Watanabe, M. (2010). An SMT approach to bounded model checking of design in state transition matrix. In A. Iglesias, O. Gervasi, M. L. Gavrilova, D. Taniar, & B. O. Apduhan (Eds.), Proceedings - 2010 10th International Conference on Computational Science and Its Applications, ICCSA 2010 (pp. 231-238). (Proceedings - 2010 10th International Conference on Computational Science and Its Applications, ICCSA 2010). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/ICCSA.2010.57

An SMT approach to bounded model checking of design in state transition matrix. / Kong, Weiqiang; Shiraishi, Tomohiro; Mizushima, Yuki; Katahira, Noriyuki; Fukuda, Akira; Watanabe, Masahiko.

Proceedings - 2010 10th International Conference on Computational Science and Its Applications, ICCSA 2010. ed. / Andres Iglesias; Osvaldo Gervasi; Marina L. Gavrilova; David Taniar; Bernady O. Apduhan. Institute of Electrical and Electronics Engineers Inc., 2010. p. 231-238 (Proceedings - 2010 10th International Conference on Computational Science and Its Applications, ICCSA 2010).

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

Kong, W, Shiraishi, T, Mizushima, Y, Katahira, N, Fukuda, A & Watanabe, M 2010, An SMT approach to bounded model checking of design in state transition matrix. in A Iglesias, O Gervasi, ML Gavrilova, D Taniar & BO Apduhan (eds), Proceedings - 2010 10th International Conference on Computational Science and Its Applications, ICCSA 2010. Proceedings - 2010 10th International Conference on Computational Science and Its Applications, ICCSA 2010, Institute of Electrical and Electronics Engineers Inc., pp. 231-238, 10th International Conference on Computational Science and Its Applications, ICCSA 2010, Fukuoka, Japan, 3/23/10. https://doi.org/10.1109/ICCSA.2010.57
Kong W, Shiraishi T, Mizushima Y, Katahira N, Fukuda A, Watanabe M. An SMT approach to bounded model checking of design in state transition matrix. In Iglesias A, Gervasi O, Gavrilova ML, Taniar D, Apduhan BO, editors, Proceedings - 2010 10th International Conference on Computational Science and Its Applications, ICCSA 2010. Institute of Electrical and Electronics Engineers Inc. 2010. p. 231-238. (Proceedings - 2010 10th International Conference on Computational Science and Its Applications, ICCSA 2010). https://doi.org/10.1109/ICCSA.2010.57
Kong, Weiqiang ; Shiraishi, Tomohiro ; Mizushima, Yuki ; Katahira, Noriyuki ; Fukuda, Akira ; Watanabe, Masahiko. / An SMT approach to bounded model checking of design in state transition matrix. Proceedings - 2010 10th International Conference on Computational Science and Its Applications, ICCSA 2010. editor / Andres Iglesias ; Osvaldo Gervasi ; Marina L. Gavrilova ; David Taniar ; Bernady O. Apduhan. Institute of Electrical and Electronics Engineers Inc., 2010. pp. 231-238 (Proceedings - 2010 10th International Conference on Computational Science and Its Applications, ICCSA 2010).
@inproceedings{2e00f17e04124d09ab96e8c9c0c00659,
title = "An SMT approach to bounded model checking of design in state transition matrix",
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.",
author = "Weiqiang Kong and Tomohiro Shiraishi and Yuki Mizushima and Noriyuki Katahira and Akira Fukuda and Masahiko Watanabe",
year = "2010",
month = "1",
day = "1",
doi = "10.1109/ICCSA.2010.57",
language = "English",
series = "Proceedings - 2010 10th International Conference on Computational Science and Its Applications, ICCSA 2010",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "231--238",
editor = "Andres Iglesias and Osvaldo Gervasi and Gavrilova, {Marina L.} and David Taniar and Apduhan, {Bernady O.}",
booktitle = "Proceedings - 2010 10th International Conference on Computational Science and Its Applications, ICCSA 2010",
address = "United States",

}

TY - GEN

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

AU - Kong, Weiqiang

AU - Shiraishi, Tomohiro

AU - Mizushima, Yuki

AU - Katahira, Noriyuki

AU - Fukuda, Akira

AU - Watanabe, Masahiko

PY - 2010/1/1

Y1 - 2010/1/1

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

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

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

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

U2 - 10.1109/ICCSA.2010.57

DO - 10.1109/ICCSA.2010.57

M3 - Conference contribution

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

SP - 231

EP - 238

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

A2 - Iglesias, Andres

A2 - Gervasi, Osvaldo

A2 - Gavrilova, Marina L.

A2 - Taniar, David

A2 - Apduhan, Bernady O.

PB - Institute of Electrical and Electronics Engineers Inc.

ER -