ISCAS OpenIR  > 基础软件与系统重点实验室
基于Yices对时间自动机的有界模型检测
其他题名bounded model checking of timed automata based on yices
王晓亮
2010
发表期刊计算机工程与设计
ISSN1000-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.
条目包含的文件
文件名称/大小 文献类型 版本类型 开放类型 使用许可
基于Yices对时间自动机的有界模型检测(376KB) 开放获取--请求全文
个性服务
推荐该条目
保存到收藏夹
查看访问统计
导出为Endnote文件
谷歌学术
谷歌学术中相似的文章
[王晓亮]的文章
百度学术
百度学术中相似的文章
[王晓亮]的文章
必应学术
必应学术中相似的文章
[王晓亮]的文章
相关权益政策
暂无数据
收藏/分享
所有评论 (0)
暂无评论
 

除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。