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

被引：150

作者：

林惠民

张文辉

机构：

[1] 中国科学院软件研究所

[2] 中国科学院软件研究所北京

[3] 北京

来源：

电子学报 | 2002年 / S1期

关键词：

系统可靠性; 模态/时序逻辑; 模型检测;

D O I：

暂无

中图分类号：

TP311.1 [程序设计];

学科分类号：

摘要：

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

引用

页码：1907 / 1912

页数：6

共 13 条

[1] Finite-state analysis of two contract signing protocols [J].

Shmatikov, V ;

Mitchell, JC .

THEORETICAL COMPUTER SCIENCE, 2002, 283 (02) :419-450

[2]

SMC[J] . A. Prasad Sistla,Viktor Gyuris,E. Allen Emerson.ACM Transactions on Software Engineering and Methodology (TOSEM) . 2000 (2)

[3]

Issues in slicing PROMELA and its applications to model checking, protocol understanding, and simulation[J] . Lynette I. Millett,Tim Teitelbaum.International Journal on Software Tools for Technology Transfer . 2000 (4)

[4] A minimized automaton representation of reachable states [J].