Checking RTECTL properties of STSs via SMT-based Bounded Model Checking
We present an SMT-based bounded model checking (BMC) method for Simply-Timed Systems (STSs) and for the existential fragment of the Real-time Computation Tree Logic. We implemented the SMT-based BMC algorithm and compared it with the SAT-based BMC method for the same systems and the same property la...
| 發表在: | International Journal of Interactive Multimedia and Artificial Intelligence |
|---|---|
| Main Authors: | , |
| 格式: | Article |
| 語言: | 英语 |
| 出版: |
Universidad Internacional de La Rioja (UNIR)
2015-12-01
|
| 主題: | |
| 在線閱讀: | http://www.ijimai.org/journal/node/858 |