改进的以SMT为基础的实时系统限界模型检测

	改进的以SMT为基础的实时系统限界模型检测
其他题名	improved smt-based bounded model checking for real-time systems
	徐亮
	2010
发表期刊	软件学报
ISSN	1000-9825
卷号	21 期号:7 页码:1491-1502
摘要	基于SAT的限界模型检测在处理实时系统时具有很高的复杂度.SMT求解器在计算可满足性的同时,还能处理算术和其他可判定性理论.在对实时系统进行检测时,用SMT求解器代替SAT求解器,系统里的时钟就可以用整型或实型变量表示,时钟约束则可以直接表示成线性算术表达式,从而使整个检测过程更加高效.带时间参数的计算树逻辑(timed computation tree logic,简称TCTL)被用来描述实时系统里的性质.同时,还对检测方法作了相应的改进.
关键词	限界模型检测可满足性模块理论实时系统时间自动机时间kripke结构带时间参数的计算树逻辑bounded Model Checking Satisfiability Modulo Theories Real-time System Timed Automata Timed Kripke Structure Tctl (Timed Computation Tree Logic)
部门归属	中国科学院软件研究所计算机科学国家重点实验室;中国科学院软件研究所;
学科领域	Computer Science
内容类型	期刊论文
URI标识	http://ir.iscas.ac.cn/handle/311060/9846
专题	基础软件与系统重点实验室
推荐引用方式 GB/T 7714	徐亮. 改进的以SMT为基础的实时系统限界模型检测[J]. 软件学报,2010,21(7):1491-1502.
APA	徐亮.(2010).改进的以SMT为基础的实时系统限界模型检测.软件学报,21(7),1491-1502.
MLA	徐亮."改进的以SMT为基础的实时系统限界模型检测".软件学报 21.7(2010):1491-1502.

条目包含的文件
文件名称/大小	文献类型	版本类型	开放类型	使用许可
改进的以SMT为基础的实时系统限界模型检（631KB）			开放获取	--	请求全文