电子学报 ›› 2002, Vol. 30 ›› Issue (S1): 1907-1912.

• 综述评论 • 上一篇    下一篇

模型检测:理论、方法与应用

林惠民, 张文辉   

  1. 中国科学院软件研究所, 北京, 100080
  • 收稿日期:2002-08-16 修回日期:2002-10-16 出版日期:2002-12-25 发布日期:2002-12-25
  • 作者简介:林惠民 男,1947年11月出生于福建福州,1986年在中国科学院软件所获博士学位,现任中国科学院软件研究所计算机科学重点实验室研究员、主任,研究兴趣包括:并发理论及应用、模型检测、进程代数、移动计算的形式模型与分析、形式化方法.张文辉 男,1963年6月出生于福建福安,1988年在挪威奥斯陆大学数学自然科学学院获博士学位,现任中国科学院软件研究所计算机科学重点实验室研究员,研究兴趣包括:程序正确性、模型检测、逻辑推理、形式化方法.
  • 基金资助:

    国家自然科学基金(No.6983320)

Model Checking: Theories, Techniques and Applications

LIN Hui-min, ZHANG Wen-hui   

  1. Institute of Software, Chinese Academy of Sciences, Beijing 100080, China
  • Received:2002-08-16 Revised:2002-10-16 Online:2002-12-25 Published:2002-12-25

摘要: 随着计算机软硬件系统日益复杂,如何保证其正确性和可靠性成为日益紧迫的问题.在为此提出的诸多理论和方法中,模型检测(model checking)以其简洁明了和自动化程度高而引人注目.模型检测的研究大致涵盖以下内容:模态/时序逻辑、模型检测算法及其时空效率(特别是空间效率)的改进以及支撑工具的研制.这几个方面之间有着密切的内在联系.不同模态/时序逻辑的模型检测算法的复杂性不一样,优化算法往往是针对某些特定类型的逻辑公式.本文将就这几个方面分别加以阐述,最后介绍该领域的新进展.

关键词: 系统可靠性, 模态/时序逻辑, 模型检测

Abstract: As computer hardware and software systems become more and more complex,how to assure the correctness and reliability of such system sbecomes an urgent problem. Among theories proposed as solutions to this problem, model checking has become a very attractive and appealing approach, because of its simplicity and high level of automation. Research on model checking covers the following subjects: modal/temporal logics, model checking algorithms, efficiency of model checking with respect to time and space(especially space complexity), and development of model checking tools. These aspects are closely related. Complexities of model checking algorithms vary very much for different modal/temporal logics, and optimizations are often targeted at certain types of logic fonnulas. Some new achievements and research directions are also discussed.

Key words: system reliability, modal/temporal logics, model checking

中图分类号: