基于SMT的TECTL性质的限界模型检测方法

• 作者: 刘宏 徐亮
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 限界模型检测 可满足性模理论 全局性性质 实时系统 验证
• 年，卷（期）: 2013,（10）
• 所属期刊栏目: 软件工程
• 页码范围: 166-171
• 页数: 6页
• 分类号: TP301.2
• 字数: 4984字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2013.10.023

摘要

近些年来,基于SMT的限界模型检测方法作为基于SAT的限界模型检测方法的一种改进,在对实时系统的检测上已经得到了一定发展.一直以来,限界模型检测多被用于检验存在性性质,而很少用于验证全局性性质,原因之一就是该方法受界限的限制,很难实现对全局性性质的有效编码.为此,通过对传统限界模型检测中的编码方式进行相应改变,在一定程度上解决了这一问题.同时,结合SMT,实现了对实时系统中某些全局性性质的验证.实验表明该方法比已有的方法效率更高.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	徐亮	湖南师范大学数学与计算机科学学院	9	50	3.0	7.0
2	刘宏		2	2	1.0	1.0