基于Yices对时间自动机的有界模型检测
文献类型：期刊论文
| 作者 | 王晓亮 |
| 刊名 | 计算机工程与设计
 |
| 出版日期 | 2010 |
| 卷号 | 31期号:1页码:126-129 |
| 关键词 | 有界模型检测 时间自动机 SMT工具 可达性 安全性 逻辑公式bounded model checking timed automata SMT tools reaehability safety logic formula |
| ISSN号 | 1000-7024 |
| 其他题名 | bounded model checking of timed automata based on yices |
| 中文摘要 | 为了避免在有界模型检测过程中对变量进行布尔编码以及对时间自动机模型中的时钟进行预处理,给出一个利用SMT(satisfiability modulo theories)工具进行的对时间自动机进行有界模型检测的方法。该方法将时间自动机模型直接转换成SMT工具可识别的逻辑公式,利用SMT工具可求解包含有整数型和实数型变量逻辑公式的能力来进行模型检测。实验结果表明,对于某些可达性性质的验证,该方法的效率有一定的优势。 |
| 学科主题 | Computer Science |
| 语种 | 中文 |
| 公开日期 | 2011-05-23 |
| 附注 | To avoid encoding variants in the model into boolean type in the process ofbounded model checking(BMC)and prcprocessing clocksfortimedautomata(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 results that,for some verification of reachability,the presented method has better performance. |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/9874]  |
| 专题 | 软件研究所_计算机科学国家重点实验室 _期刊论文 |
| 推荐引用方式 GB/T 7714 | 王晓亮. 基于Yices对时间自动机的有界模型检测[J]. 计算机工程与设计,2010,31(1):126-129. |
| APA | 王晓亮.(2010).基于Yices对时间自动机的有界模型检测.计算机工程与设计,31(1),126-129. |
| MLA | 王晓亮."基于Yices对时间自动机的有界模型检测".计算机工程与设计 31.1(2010):126-129. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。