| 本文已被：浏览 1910次 下载 5164次 |
码上扫一扫！ |
|
|
| 基于时态测试器的实时分支时态逻辑模型检测 |
|
骆翔宇1,2, 黄欣玥1, 古天龙2,3, 苏开乐4, 陈祖希1, 郑黎晓1
|
|
1.华侨大学 计算机科学与技术学院, 福建 厦门 361021;2.广西可信软件重点实验室(桂林电子科技大学), 广西 桂林 541004;3.暨南大学 信息科学技术学院/网络空间安全学院, 广东 广州 510632;4.南京信息工程大学 人工智能学院, 江苏 南京 210044
|
|
| 摘要: |
| 基于自动机理论的模型检测技术在形式化验证领域处于核心地位,然而传统自动机在时态算子上不具备可组合性,导致各种时态逻辑的模型检测算法不能有机整合.为了实现集成限界时态算子的实时分支时态逻辑RTCTL*的高效模型检测,提出一种RTCTL*正时态测试器构造方法以及相关符号化模型检测算法,既证明了所提出的RTCTL*正时态测试器构造方法是完备的,也证明了该算法时间复杂度与被验证系统呈线性关系,与公式长度呈指数关系.基于JavaBDD软件包成功开发了该算法的模型检测工具MCTK 2.0.0.完成了MCTK与著名的符号化模型检测工具nuXmv之间的实验对比分析工作,结果表明:MCTK虽然在内存消耗上要多于nuXmv,但是MCTK的时间复杂度双指数级小于nuXmv,使得利用MCTK验证大规模系统的实时时态性质成为可能. |
| 关键词: 符号化模型检测 公平离散系统 正时态测试器 实时分支时态逻辑 二元决策图 |
| DOI：10.13328/j.cnki.jos.006606 |
| 分类号:TP311 |
| 基金项目:国家自然科学基金(U1711263,1966009,62006057,61170028);福建省自然科学基金(2021J01316,2021J01320,2015J01255);广西可信软件重点实验室研究课题(kx201323) |
|
| Model Checking for Real-time Branching-time Temporal Logic Based on Temporal Testers |
|
LUO Xiang-Yu1,2, HUANG Xin-Yue1, GU Tian-Long2,3, SU Kai-Le4, CHEN Zu-Xi1, ZHENG Li-Xiao1
|
|
1.College of Computer Science and Technology, Huaqiao University, Xiamen 361021, China;2.Guangxi Key Laboratory of Trusted Software (Guilin University of Electronic Technology), Guilin 541004, China;3.College of Information Science and Technology/College of Cyber Security, Jinan University, Guangzhou 510632, China;4.School of Artificial Intelligence, Nanjing University of Information Science & Technology, Nanjing 210044, China
|
| Abstract: |
| Model checking techniques based on automata theory play a central role in formal verification. Nevertheless, classical automata are not composable for temporal operators, such that the model checking algorithms for various temporal logics cannot be organically integrated. To realize efficient model checking for real-time branching-time temporal logic RTCTL* integrating bounded temporal operators, a construction method is proposed for RTCTL* positive temporal testers, and the RTCTL* symbolic model checking algorithm is further proposed based on positive temporal testers. It is proved that the proposed construction method for RTCTL* positive temporal testers is complete. It is also proved that the time complexity of the proposed algorithm is linear in the size of the verified system and exponential in the length of the given formula. Based on the JavaBDD software package, the model checking tool MCTK 2.0.0 is successfully developed for the proposed algorithm. The experimental data and the analysis results show that although MCTK consumes more memory than the famous symbolic model checker nuXmv, the time complexity of MCTK is doubly-exponentially less than nuXmv, which makes it possible to verify real-time temporal properties of large-scale systems by MCTK. |
| Key words: symbolic model checking just discrete system positive temporal tester real-time branching-time temporal logic binary decision diagram |
