ISCAS OpenIR  > 基础软件与系统重点实验室
基于Yices对时间自动机的有界模型检测
Alternative Titlebounded model checking of timed automata based on yices
王晓亮
2010
Source计算机工程与设计
ISSN1000-7024
Volume31Issue:1Pages:126-129
English Abstract为了避免在有界模型检测过程中对变量进行布尔编码以及对时间自动机模型中的时钟进行预处理,给出一个利用SMT(satisfiability modulo theories)工具进行的对时间自动机进行有界模型检测的方法。该方法将时间自动机模型直接转换成SMT工具可识别的逻辑公式,利用SMT工具可求解包含有整数型和实数型变量逻辑公式的能力来进行模型检测。实验结果表明,对于某些可达性性质的验证,该方法的效率有一定的优势。
Keyword有界模型检测 时间自动机 Smt工具 可达性 安全性 逻辑公式bounded Model Checking Timed Automata Smt Tools Reaehability Safety Logic Formula
Department中国科学院软件研究所计算机科学国家重点实验室;中国科学院研究生院;
SubjectComputer Science
Language中文
Content Type期刊论文
URIhttp://ir.iscas.ac.cn/handle/311060/9874
Collection基础软件与系统重点实验室
Recommended Citation
GB/T 7714
王晓亮. 基于Yices对时间自动机的有界模型检测[J]. 计算机工程与设计,2010,31(1):126-129.
APA 王晓亮.(2010).基于Yices对时间自动机的有界模型检测.计算机工程与设计,31(1),126-129.
MLA 王晓亮."基于Yices对时间自动机的有界模型检测".计算机工程与设计 31.1(2010):126-129.
Files in This Item:
File Name/Size DocType Version Access License
基于Yices对时间自动机的有界模型检测(376KB) 开放获取--Application Full Text
Related Services
Recommend this item
Bookmark
Usage statistics
Export to Endnote
Google Scholar
Similar articles in Google Scholar
[王晓亮]'s Articles
Baidu academic
Similar articles in Baidu academic
[王晓亮]'s Articles
Bing Scholar
Similar articles in Bing Scholar
[王晓亮]'s Articles
Terms of Use
No data!
Social Bookmark/Share
All comments (0)
No comment.
 

Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.