首页 | 本学科首页   官方微博 | 高级检索  
     

模型检测:理论、方法与应用
引用本文:林惠民,张文辉.模型检测:理论、方法与应用[J].电子学报,2002,30(Z1):1907-1912.
作者姓名:林惠民  张文辉
作者单位:中国科学院软件研究所, 北京, 100080
基金项目:国家自然科学基金,6983320,
摘    要:随着计算机软硬件系统日益复杂,如何保证其正确性和可靠性成为日益紧迫的问题.在为此提出的诸多理论和方法中,模型检测(model checking)以其简洁明了和自动化程度高而引人注目.模型检测的研究大致涵盖以下内容:模态/时序逻辑、模型检测算法及其时空效率(特别是空间效率)的改进以及支撑工具的研制.这几个方面之间有着密切的内在联系.不同模态/时序逻辑的模型检测算法的复杂性不一样,优化算法往往是针对某些特定类型的逻辑公式.本文将就这几个方面分别加以阐述,最后介绍该领域的新进展.

关 键 词:系统可靠性  模态/时序逻辑  模型检测  
文章编号:0372-2112(2002)12A-1907-06
收稿时间:2002-08-16
修稿时间:2002年8月16日

Model Checking: Theories,Techniques and Applications
LIN Hui-min,ZHANG Wen-hui.Model Checking: Theories,Techniques and Applications[J].Acta Electronica Sinica,2002,30(Z1):1907-1912.
Authors:LIN Hui-min  ZHANG Wen-hui
Affiliation:Institute of Software, Chinese Academy of Sciences, Beijing 100080, China
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.
Keywords:system reliability  modal/temporal logics  model checking
本文献已被 万方数据 等数据库收录!
点击此处可从《电子学报》浏览原始摘要信息
点击此处可从《电子学报》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号