浅析模型检测技术

A Brief Analysis of Model Checking Technique

模型检测是一种能够自动验证有限状态并发系统技术。通过显式状态搜索来验证有限状态并发系统的模态与命题性质,当前已被广泛应用于计算机软硬件系统安全性能的检测。本文浅析了模型检测技术,分析了模型检测技术的发展概况、基本原理、算法、模型检测工具等,并介绍了模型检测领域的最新进展。

Model checking is a technique for automatically verifying correctness properties of the finite state concurrent systems. It verifies modality and propositional property of finite state concurrent systems according to explicit state search results. In the current, model checking technique has been widely used to verify safety performance of computer software and hardware system. In this paper, we give a brief analysis of model checking technique. The development of model checking, basic principle of model checking, algorithm of symbolic model checking and model checking tools have been introduced. Finally, we introduce the latest developments in model checking field.