基于Yices对时间自动机的有界模型检测

	基于Yices对时间自动机的有界模型检测
Alternative Title	bounded model checking of timed automata based on yices
	王晓亮
	2010
Source	计算机工程与设计
ISSN	1000-7024
Volume	31 Issue:1 Pages:126-129
English Abstract	为了避免在有界模型检测过程中对变量进行布尔编码以及对时间自动机模型中的时钟进行预处理,给出一个利用SMT(satisfiability modulo theories)工具进行的对时间自动机进行有界模型检测的方法。该方法将时间自动机模型直接转换成SMT工具可识别的逻辑公式,利用SMT工具可求解包含有整数型和实数型变量逻辑公式的能力来进行模型检测。实验结果表明,对于某些可达性性质的验证,该方法的效率有一定的优势。
Keyword	有界模型检测时间自动机 Smt工具可达性安全性逻辑公式bounded Model Checking Timed Automata Smt Tools Reaehability Safety Logic Formula
Department	中国科学院软件研究所计算机科学国家重点实验室;中国科学院研究生院;
Subject	Computer Science
Language	中文
Content Type	期刊论文
URI	http://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

If you have any objections to this item, please fill out the form below and the administrator will contact you as soon as possible.
Content:
Email：	*
Institution:
Verification Code:	Refresh

Any comments and suggestions are welcomed.
Title:	*
Content:
Email：	*
Verification Code:	Refresh

中国科学院软件研究所机构知识库