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

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