基于时态测试器的实时分支时态逻辑模型检测

来源：软件学报杂志2022年第8期北京时间：

作者：骆翔宇，黄欣玥，古天龙，苏开乐，陈祖希，郑黎晓

单位：骆翔宇，华侨大学 计算机科学与技术学院, 福建 厦门 361021;广西可信软件重点实验室(桂林电子科技大学), 广西 桂林 54100411,黄欣玥，华侨大学 计算机科学与技术学院, 福建 厦门 36102102,古天龙，广西可信软件重点实验室(桂林电子科技大学), 广西 桂林 541004;暨南大学 信息科学技术学院/网络空间安全学院, 广东 广州 51063203,苏开乐，南京信息工程大学 人工智能学院, 江苏 南京 21004404,陈祖希，华侨大学 计算机科学与技术学院, 福建 厦门 36102105,郑黎晓，华侨大学 计算机科学与技术学院, 福建 厦门 36102106

摘要：基于自动机理论的模型检测技术在形式化验证领域处于核心地位,然而传统自动机在时态算子上不具备可组合性,导致各种时态逻辑的模型检测算法不能有机整合.为了实现集成限界时态算子的实时分支时态逻辑RTCTL*的高效模型检测,提出一种RTCTL*正时态测试器构造方法以及相关符号化模型检测算法,既证明了所提出的RTCTL*正时态测试器构造方法是完备的,也证明了该算法时间复杂度与被验证系统呈线性关系,与公式长度呈指数关系.基于JavaBDD软件包成功开发了该算法的模型检测工具MCTK 2.0.0.完成了MCTK与著名的符号化模型检测工具nuXmv之间的实验对比分析工作,结果表明:MCTK虽然在内存消耗上要多于nuXmv,但是MCTK的时间复杂度双指数级小于nuXmv,使得利用MCTK验证大规模系统的实时时态性质成为可能.

关键词：符号化模型检测;公平离散系统;正时态测试器;实时分支时态逻辑;二元决策图

基金资助：国家自然科学基金(U1711263,1966009,62006057,61170028);福建省自然科学基金(2021J01316,2021J01320,2015J01255);广西可信软件重点实验室研究课题(kx201323)