ISCAS OpenIR  > 基础软件与系统重点实验室
改进的以SMT为基础的实时系统限界模型检测
其他题名improved smt-based bounded model checking for real-time systems
徐亮
2010
发表期刊软件学报
ISSN1000-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) 开放获取--请求全文
个性服务
推荐该条目
保存到收藏夹
查看访问统计
导出为Endnote文件
谷歌学术
谷歌学术中相似的文章
[徐亮]的文章
百度学术
百度学术中相似的文章
[徐亮]的文章
必应学术
必应学术中相似的文章
[徐亮]的文章
相关权益政策
暂无数据
收藏/分享
所有评论 (0)
暂无评论
 

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