典型文献
基于时态测试器的实时分支时态逻辑模型检测
文献摘要：
基于自动机理论的模型检测技术在形式化验证领域处于核心地位,然而传统自动机在时态算子上不具备可组合性,导致各种时态逻辑的模型检测算法不能有机整合.为了实现集成限界时态算子的实时分支时态逻辑RTCTL*的高效模型检测,提出一种RTCTL*正时态测试器构造方法以及相关符号化模型检测算法,既证明了所提出的RTCTL*正时态测试器构造方法是完备的,也证明了该算法时间复杂度与被验证系统呈线性关系,与公式长度呈指数关系.基于JavaBDD软件包成功开发了该算法的模型检测工具MCTK 2.0.0.完成了MCTK与著名的符号化模型检测工具nuXmv之间的实验对比分析工作,结果表明:MCTK虽然在内存消耗上要多于nuXmv,但是MCTK的时间复杂度双指数级小于nuXmv,使得利用MCTK验证大规模系统的实时时态性质成为可能.
文献关键词：
符号化模型检测;公平离散系统;正时态测试器;实时分支时态逻辑;二元决策图
中图分类号：
作者姓名：
骆翔宇;黄欣玥;古天龙;苏开乐;陈祖希;郑黎晓
作者机构：
华侨大学 计算机科学与技术学院, 福建 厦门 361021;广西可信软件重点实验室(桂林电子科技大学), 广西 桂林 541004;暨南大学 信息科学技术学院/网络空间安全学院, 广东 广州 510632;南京信息工程大学 人工智能学院, 江苏 南京 210044
文献出处：
引用格式：
[1]骆翔宇;黄欣玥;古天龙;苏开乐;陈祖希;郑黎晓-.基于时态测试器的实时分支时态逻辑模型检测)[J].软件学报,2022(08):2930-2946
A类：
实时分支时态逻辑,RTCTL,正时态测试器,符号化模型检测,JavaBDD,MCTK,nuXmv,公平离散系统
B类：
逻辑模型,自动机,动机理论,形式化验证,核心地位,可组合,组合性,检测算法,有机整合,限界,构造方法,时间复杂度,验证系统,软件包,包成,检测工具,实验对比,分析工作,双指数,数级,得利,大规模系统,时时,质成,二元决策图
AB值：
0.197904
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
