微信服务号

微信订阅号

2025年3月30日 14:12 星期日
首页 > 过刊浏览>2022年第33卷第8期 >2930-2946. DOI:10.13328/j.cnki.jos.006606
PDF HTML阅读 XML下载 导出引用 引用提醒
基于时态测试器的实时分支时态逻辑模型检测
作者:
作者简介:

骆翔宇(1974－),男,博士,副教授,CCF专业会员,主要研究领域为形式化方法,模型检测,时态逻辑,多智能体系统;
苏开乐(1964－),男,博士,教授,博士生导师,CCF高级会员,主要研究领域为形式化方法,模型检测,多智能体系统,难解问题的算法设计;
黄欣玥(1994－),女,硕士生,CCF学生会员,主要研究领域为形式化方法,模型检测,时态逻辑;
陈祖希(1981－),男,博士,讲师,CCF专业会员,主要研究领域为形式化方法,程序验证,软硬件系统安全评估;
古天龙(1964－),男,博士,教授,博士生导师,CCF高级会员,主要研究领域为形式化方法,人工智能安全,人工智能伦理,数据治理;
郑黎晓(1983－),女,博士,副教授,CCF专业会员,主要研究领域为形式语言与自动机,数据库理论,软件测试.

通讯作者:

郑黎晓,E-mail:zheng_lixiao@163.com

中图分类号:

TP311

基金项目:

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


Model Checking for Real-time Branching-time Temporal Logic Based on Temporal Testers
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [21]
    • |
  • 相似文献
    • | | |
  • 文章评论
    摘要:

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

    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.

    参考文献
    [1] Clarke EM, Grumberg O, Kroening D, et al.Model Checking.2nd ed., Cambridge:MIT Press, 2018.
    [2] Clarke EM, Henzinger TA, Veith H, et al.Handbook of Model Checking.Cham:Springer, 2018.[doi:10.1007/978-3-319-10575-8]
    [3] IEEE Computer Society.IEEE Standard for Property Specification Language (PSL).IEEE Std 1850-2010(Revision of IEEE Std 1850-2005), 2010.1-182.[doi:10.1109/IEEESTD.2010.5446004]
    [4] IEEE Computer Society and the IEEE Standards Association Corporate Advisory Group.IEEE Standard for SystemVerilog-Unified Hardware Design, Specification, and Verification Language.IEEE Std 1800-2017(Revision of IEEE Std 1800-2012), 2018.1-1315.[doi:10.1109/IEEESTD.2018.8299595]
    [5] Pnueli A, Zaks A.On the merits of temporal testers.In:Grumberg O, Veith H, eds.Proc.of the 25 Years of Model Checking.Berlin, Heidelberg:Springer, 2008.172-195.[doi:10.1007/978-3-540-69850-0_11]
    [6] Luo XY, Wu LJ, Chen QL, et al.Symbolic model checking for discrete real-time systems.Science China Information Science, 2018, 61(5):052106:1-052106:23.[doi:10.1007/s11432-017-9152-x]
    [7] Kesten Y, Pnueli A, Raviv L.Algorithmic verification of linear temporal logic specifications.In:Larsen KG, Skyum S, Winskel G, eds.Proc.of the 25th Int'l Colloquium on Automata, Languages and Programming.Berlin, Heidelberg:Springer, 1998.1-16.[doi:10.5555/646252.756784]
    [8] Bryant RE.Graph-Based algorithms for boolean function manipulation.IEEE Trans.on Computers, 1986, 35(8):677-691.[doi:10.1109/TC.1986.1676819]
    [9] Maler O, Nickovic D, Pnueli A.From MITL to timed automata.In:Asarin E, BouyerP, eds.Proc.of the FORMATS 2006.Berlin, Heidelberg:Springer, 2006.274-289.[doi:10.1007/11867340_20]
    [10] Cimatti A, Clarke E, Giunchiglia E, et al.Nusmv 2:An opensource tool for symbolic model checking.In:Brinksma E, Larsen KG, eds.Proc.of the CAV 2002.Berlin, Heidelberg:Springer, 2002.359-364.[doi:10.1007/3-540-45657-0_29]
    [11] Cavada R, Cimatti A, Dorigatti M, et al.The nuXmv symbolic model checker.In:Biere A, Bloem R, eds.Proc.of the CAV 2014.Berlin, Heidelberg:Springer, 2014.334-342.[doi:10.1007/978-3-319-08867-9_22]
    [12] Lomuscio A, Qu HY, Raimondi F.MCMAS:An open-source model checker for the verification of multi-agent systems.Int'l Journal on Software Tools for Technology Transfer, 2017, 19(1):9-30.[doi:10.1007/s10009-015-0378-x]
    [13] Su KL, Sattar A, Luo XY.Model checking temporal logics of knowledge via OBDDs.The Computer Journal, 2007, 50(4):403-420.[doi:10.1093/comjnl/bxm009]
    [14] Alur R, Henzinger TA.Real-time logics:Complexity and expressiveness.Information and Computation, 1993, 104(1):35-77.[doi:10.1006/inco.1993.1025]
    [15] Alur R, Henzinger TA.A really temporal logic.Journal of the ACM, 1994, 41(1):181-203.[doi:10.1145/174644.174651]
    [16] Larsen KG, Pettersson P, Wang Y.UPPAAL in a nutshell.Int'l Journal on Software Tools for Technology Transfer, 1997, 1(1-2):134-152.[doi:10.1007/s100090050010]
    [17] Henzinger TA, Ho PH, Wong-Toi H.HYTECH:A model checker for hybrid systems.Int'l Journal on Software Tools for Technology Transfer, 1997, 1:110-122.[doi:10.1007/s100090050008]
    [18] Bozga M, Daws C, Maler O, et al.Kronos:A model-checking tool for real-time systems.In:Hu AJ, Vardi MY, eds.Proc.of the CAV'98.Berlin, Heidelberg:Springer, 1998.546-550.[doi:10.1007/BFb0028779]
    [19] Georges M, Christoph S.Fully symbolic TCTL model checking for complete and incomplete real-time systems.Science of Computer Programming, 2015, 111:248-276.[doi:10.1016/j.scico.2015.08.002]
    [20] McMillan KL.The SMV system-For SMV version 2.5.4.Carnegie Mellon University, 2000.https://www.cs.cmu.edu/~modelcheck/smv/smvmanual.ps
    [21] Gabbay DM, Pnueli A.A sound and complete deductive system for CTL* verification.Logic Journal of the IGPL, 2008, 16(6):499-536.[doi:10.1093/jigpal/jzn018]
    相似文献
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

骆翔宇,黄欣玥,古天龙,苏开乐,陈祖希,郑黎晓.基于时态测试器的实时分支时态逻辑模型检测.软件学报,2022,33(8):2930-2946

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2021-09-06
  • 最后修改日期:2021-10-14
  • 在线发布日期: 2022-01-28
  • 出版日期: 2022-08-06
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号