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

	改进的以SMT为基础的实时系统限界模型检测
	徐亮
刊名	软件学报
	2010
卷号	21 期号:7 页码:1491-1502
关键词	限界模型检测可满足性模块理论实时系统时间自动机时间Kripke结构带时间参数的计算树逻辑bounded model checking satisfiability modulo theories real-time system timed automata timed Kripke structure TCTL (timed computation tree logic)
ISSN号	1000-9825
其他题名	improved smt-based bounded model checking for real-time systems
中文摘要	基于SAT的限界模型检测在处理实时系统时具有很高的复杂度.SMT求解器在计算可满足性的同时,还能处理算术和其他可判定性理论.在对实时系统进行检测时,用SMT求解器代替SAT求解器,系统里的时钟就可以用整型或实型变量表示,时钟约束则可以直接表示成线性算术表达式,从而使整个检测过程更加高效.带时间参数的计算树逻辑(timed computation tree logic,简称TCTL)被用来描述实时系统里的性质.同时,还对检测方法作了相应的改进.
学科主题	Computer Science
公开日期	2011-05-23
附注	SAT-Based bounded model checking (BMC) has high complexity in dealing with real-time systems. Satisfiability modulo theories (SMT) solvers can generalize SAT solving by adding the ability to handle arithmetic and other decidable theories. This paper uses SMT in BMC for real-time systems instead of SAT. The clocks can be represented as integer or real variables directly and clock constraints can be represented as linear arithmetic expressions. These make the checking procedure more efficient. TCTL (timed computation tree logic) is used to specify the properties of real-time systems and improvement of the encodings has been done.
内容类型	期刊论文
源URL	[http://124.16.136.157/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.