| 基于Yices对时间自动机的有界模型检测 |
| |
| 引用本文： | 王晓亮. 基于Yices对时间自动机的有界模型检测[J]. 计算机工程与设计, 2010, 31(1) |
| |
| 作者姓名： | 王晓亮 |
| |
| 作者单位： | 中国科学院软件研究所,计算机科学国家重点实验室,北京,100190;中国科学院研究生院,北京,100049 |
| |
| 摘 要： | 为了避免在有界模型检测过程中对变量进行布尔编码以及对时间自动机模型中的时钟进行预处理,给出一个利用SMT(satisfiability modulo theories)工具进行的对时间自动机进行有界模型检测的方法.该方法将时间自动机模型直接转换成SMT工具可识别的逻辑公式,利用SMT工具可求解包含有整数型和实数型变量逻辑公式的能力来进行模型检测.实验结果表明,对于某些可达性性质的验证,该方法的效率有一定的优势.
|
| 关 键 词： | 有界模型检测 时间自动机 SMT工具 可达性 安全性 逻辑公式 |
Bounded model checking of timed automata based on Yices |
| |
| WANG Xiao-liang. Bounded model checking of timed automata based on Yices[J]. Computer Engineering and Design, 2010, 31(1) |
| |
| Authors: | WANG Xiao-liang |
| |
| Affiliation: | WANG Xiao-liang1,2(1.State Key Laboratory of Computer Science,Institute of Software,Chinese Academy of Science,Beijing 100190,China,2.Graduate University,Beijing 100049,China) |
| |
| Abstract: | To avoid encoding variants in the model into boolean type in the process of bounded model checking(BMC) and preprocessing clocks for timed automata(TA),a method of BMC for timed automata based on SMT tools is presented.Timed automata is transformed into logic formula directly which is recognizable for SMT tools,and then takes advantages of the ability of SMT tools,which is SMT tool could solve the formula which includes variants of integral or real,to do checking works.It is demonstrated by experimental res... |
| |
| Keywords: | bounded model checking timed automata SMT tools reaehability safety logic formula |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
