| 基于Yices对时间自动机的有界模型检测 |
| 其他题名 | bounded model checking of timed automata based on yices
|
| 王晓亮
|
| 2010
|
| 发表期刊 | 计算机工程与设计
 |
| ISSN | 1000-7024
|
| 卷号 | 31期号:1页码:126-129 |
| 摘要 | 为了避免在有界模型检测过程中对变量进行布尔编码以及对时间自动机模型中的时钟进行预处理,给出一个利用SMT(satisfiability modulo theories)工具进行的对时间自动机进行有界模型检测的方法。该方法将时间自动机模型直接转换成SMT工具可识别的逻辑公式,利用SMT工具可求解包含有整数型和实数型变量逻辑公式的能力来进行模型检测。实验结果表明,对于某些可达性性质的验证,该方法的效率有一定的优势。 |
| 关键词 | 有界模型检测
时间自动机
Smt工具
可达性
安全性
逻辑公式bounded Model Checking
Timed Automata
Smt Tools
Reaehability
Safety
Logic Formula
|
| 部门归属 | 中国科学院软件研究所计算机科学国家重点实验室;中国科学院研究生院;
|
| 学科领域 | Computer Science
|
| 语种 | 中文
|
| 内容类型 | 期刊论文
|
| URI标识 | 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.
|
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论