Abstract
State Transition Matrix (STM) is a table-based modeling language that has been frequently used in industry for specifying behaviors of systems. Functional correctness of a STM design (i.e., a design developed with STM) could often be expressed as invariant properties. In this paper, we first present a formalization of the static and dynamic aspects of STM designs. Consequentially, based on this formalization, we investigate a symbolic encoding approach, through which a STM design could be bounded model checked w.r.t. 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. Two attempts for accelerating SMT solving are also reported.
| Original language | English |
|---|---|
| Pages (from-to) | 946-957 |
| Number of pages | 12 |
| Journal | IEICE Transactions on Information and Systems |
| Volume | E94-D |
| Issue number | 5 |
| DOIs | |
| Publication status | Published - May 2011 |
Fingerprint
All Science Journal Classification (ASJC) codes
- Software
- Hardware and Architecture
- Computer Vision and Pattern Recognition
- Electrical and Electronic Engineering
- Artificial Intelligence
Cite this
An SMT-based approach to bounded model checking of designs in state transition matrix. / Kong, Weiqiang; Shiraishi, Tomohiro; Katahira, Noriyuki; Watanabe, Masahiko; Katayama, Tetsuro; Fukuda, Akira.
In: IEICE Transactions on Information and Systems, Vol. E94-D, No. 5, 05.2011, p. 946-957.Research output: Contribution to journal › Article
}
TY - JOUR
T1 - An SMT-based approach to bounded model checking of designs in state transition matrix
AU - Kong, Weiqiang
AU - Shiraishi, Tomohiro
AU - Katahira, Noriyuki
AU - Watanabe, Masahiko
AU - Katayama, Tetsuro
AU - Fukuda, Akira
PY - 2011/5
Y1 - 2011/5
N2 - State Transition Matrix (STM) is a table-based modeling language that has been frequently used in industry for specifying behaviors of systems. Functional correctness of a STM design (i.e., a design developed with STM) could often be expressed as invariant properties. In this paper, we first present a formalization of the static and dynamic aspects of STM designs. Consequentially, based on this formalization, we investigate a symbolic encoding approach, through which a STM design could be bounded model checked w.r.t. 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. Two attempts for accelerating SMT solving are also reported.
AB - State Transition Matrix (STM) is a table-based modeling language that has been frequently used in industry for specifying behaviors of systems. Functional correctness of a STM design (i.e., a design developed with STM) could often be expressed as invariant properties. In this paper, we first present a formalization of the static and dynamic aspects of STM designs. Consequentially, based on this formalization, we investigate a symbolic encoding approach, through which a STM design could be bounded model checked w.r.t. 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. Two attempts for accelerating SMT solving are also reported.
UR - http://www.scopus.com/inward/record.url?scp=79955595443&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=79955595443&partnerID=8YFLogxK
U2 - 10.1587/transinf.E94.D.946
DO - 10.1587/transinf.E94.D.946
M3 - Article
AN - SCOPUS:79955595443
VL - E94-D
SP - 946
EP - 957
JO - IEICE Transactions on Information and Systems
JF - IEICE Transactions on Information and Systems
SN - 0916-8532
IS - 5
ER -