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
Y1 - 2011
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
T2 - 11th International Conference on Computational Science and Its Applications, ICCSA 2011
Y2 - 20 June 2011 through 23 June 2011
ER -