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

Weiqiang Kong, Noriyuki Katahira, Wanpeng Qian, Masahiko Watanabe, Tetsuro Katayama, Akira Fukuda

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

5 Citations (Scopus)

Abstract

State Transition Matrix (STM) is a table-based modeling language for developing designs of software systems. Although widely accepted and used in software industry, there is lack of formal verification supports for conducting rigorous analysis to improve reliability of STM designs. In this paper, we present a symbolic encoding approach for STM designs that employ message passing as the means of communication, through which correctness of a STM design with respect to invariant properties could be Bounded Model Checked (BMC) by using Satisfiability Modulo Theories (SMT) solving techniques. We have built a prototype implementation of the proposed encoding and the state-of-the-art SMT solver - Yices, is used in our experiments as a back-end tool to evaluate the effectiveness of our approach. In addition, two approaches for accelerating SMT solving by introducing additional knowledge are proposed and their effectiveness is shown by our preliminary experimental results.

Original languageEnglish
Title of host publicationProceedings - 2011 International Conference on Computational Science and Its Applications, ICCSA 2011
Pages159-167
Number of pages9
DOIs
Publication statusPublished - Sep 5 2011
Event11th International Conference on Computational Science and Its Applications, ICCSA 2011 - Santander, Spain
Duration: Jun 20 2011Jun 23 2011

Publication series

NameProceedings - 2011 International Conference on Computational Science and Its Applications, ICCSA 2011

Other

Other11th International Conference on Computational Science and Its Applications, ICCSA 2011
CountrySpain
CitySantander
Period6/20/116/23/11

Fingerprint

Model checking
Message passing
Computer systems
Communication
Industry
Experiments

All Science Journal Classification (ASJC) codes

  • Computational Theory and Mathematics
  • Computer Science Applications

Cite this

Kong, W., Katahira, N., Qian, W., Watanabe, M., Katayama, T., & Fukuda, A. (2011). An SMT-based approach to bounded model checking of designs in communicating state transition matrix. In Proceedings - 2011 International Conference on Computational Science and Its Applications, ICCSA 2011 (pp. 159-167). [5959550] (Proceedings - 2011 International Conference on Computational Science and Its Applications, ICCSA 2011). https://doi.org/10.1109/ICCSA.2011.30

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

Proceedings - 2011 International Conference on Computational Science and Its Applications, ICCSA 2011. 2011. p. 159-167 5959550 (Proceedings - 2011 International Conference on Computational Science and Its Applications, ICCSA 2011).

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

Kong, W, Katahira, N, Qian, W, Watanabe, M, Katayama, T & Fukuda, A 2011, An SMT-based approach to bounded model checking of designs in communicating state transition matrix. in Proceedings - 2011 International Conference on Computational Science and Its Applications, ICCSA 2011., 5959550, Proceedings - 2011 International Conference on Computational Science and Its Applications, ICCSA 2011, pp. 159-167, 11th International Conference on Computational Science and Its Applications, ICCSA 2011, Santander, Spain, 6/20/11. https://doi.org/10.1109/ICCSA.2011.30
Kong W, Katahira N, Qian W, Watanabe M, Katayama T, Fukuda A. An SMT-based approach to bounded model checking of designs in communicating state transition matrix. In Proceedings - 2011 International Conference on Computational Science and Its Applications, ICCSA 2011. 2011. p. 159-167. 5959550. (Proceedings - 2011 International Conference on Computational Science and Its Applications, ICCSA 2011). https://doi.org/10.1109/ICCSA.2011.30
Kong, Weiqiang ; Katahira, Noriyuki ; Qian, Wanpeng ; Watanabe, Masahiko ; Katayama, Tetsuro ; Fukuda, Akira. / An SMT-based approach to bounded model checking of designs in communicating state transition matrix. Proceedings - 2011 International Conference on Computational Science and Its Applications, ICCSA 2011. 2011. pp. 159-167 (Proceedings - 2011 International Conference on Computational Science and Its Applications, ICCSA 2011).
@inproceedings{0d820d4eb1454ceeacd763ac6957d315,
title = "An SMT-based approach to bounded model checking of designs in communicating state transition matrix",
abstract = "State Transition Matrix (STM) is a table-based modeling language for developing designs of software systems. Although widely accepted and used in software industry, there is lack of formal verification supports for conducting rigorous analysis to improve reliability of STM designs. In this paper, we present a symbolic encoding approach for STM designs that employ message passing as the means of communication, through which correctness of a STM design with respect to invariant properties could be Bounded Model Checked (BMC) by using Satisfiability Modulo Theories (SMT) solving techniques. We have built a prototype implementation of the proposed encoding and the state-of-the-art SMT solver - Yices, is used in our experiments as a back-end tool to evaluate the effectiveness of our approach. In addition, two approaches for accelerating SMT solving by introducing additional knowledge are proposed and their effectiveness is shown by our preliminary experimental results.",
author = "Weiqiang Kong and Noriyuki Katahira and Wanpeng Qian and Masahiko Watanabe and Tetsuro Katayama and Akira Fukuda",
year = "2011",
month = "9",
day = "5",
doi = "10.1109/ICCSA.2011.30",
language = "English",
isbn = "9780769544045",
series = "Proceedings - 2011 International Conference on Computational Science and Its Applications, ICCSA 2011",
pages = "159--167",
booktitle = "Proceedings - 2011 International Conference on Computational Science and Its Applications, ICCSA 2011",

}

TY - GEN

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

AU - Kong, Weiqiang

AU - Katahira, Noriyuki

AU - Qian, Wanpeng

AU - Watanabe, Masahiko

AU - Katayama, Tetsuro

AU - Fukuda, Akira

PY - 2011/9/5

Y1 - 2011/9/5

N2 - State Transition Matrix (STM) is a table-based modeling language for developing designs of software systems. Although widely accepted and used in software industry, there is lack of formal verification supports for conducting rigorous analysis to improve reliability of STM designs. In this paper, we present a symbolic encoding approach for STM designs that employ message passing as the means of communication, through which correctness of a STM design with respect to invariant properties could be Bounded Model Checked (BMC) by using Satisfiability Modulo Theories (SMT) solving techniques. We have built a prototype implementation of the proposed encoding and the state-of-the-art SMT solver - Yices, is used in our experiments as a back-end tool to evaluate the effectiveness of our approach. In addition, two approaches for accelerating SMT solving by introducing additional knowledge are proposed and their effectiveness is shown by our preliminary experimental results.

AB - State Transition Matrix (STM) is a table-based modeling language for developing designs of software systems. Although widely accepted and used in software industry, there is lack of formal verification supports for conducting rigorous analysis to improve reliability of STM designs. In this paper, we present a symbolic encoding approach for STM designs that employ message passing as the means of communication, through which correctness of a STM design with respect to invariant properties could be Bounded Model Checked (BMC) by using Satisfiability Modulo Theories (SMT) solving techniques. We have built a prototype implementation of the proposed encoding and the state-of-the-art SMT solver - Yices, is used in our experiments as a back-end tool to evaluate the effectiveness of our approach. In addition, two approaches for accelerating SMT solving by introducing additional knowledge are proposed and their effectiveness is shown by our preliminary experimental results.

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

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

U2 - 10.1109/ICCSA.2011.30

DO - 10.1109/ICCSA.2011.30

M3 - Conference contribution

AN - SCOPUS:80052230241

SN - 9780769544045

T3 - Proceedings - 2011 International Conference on Computational Science and Its Applications, ICCSA 2011

SP - 159

EP - 167

BT - Proceedings - 2011 International Conference on Computational Science and Its Applications, ICCSA 2011

ER -