吴迪

摘 要：模型检测作为一种形式化验证技术已成功应用于硬件以及协议的性质验证过程，目前正转向软件验证领域并逐渐扩展其应用范围。针对特定的森林防火专家系统的知识库规则，研究其所需满足的性质规范的形式化验证问题。首先将规则体描述为状态迁移图，通过引入转换函数对状态迁移图的变迁过程及状态性质进行了有效说明，然后将性质规范描述为相应的时序逻辑表达式，最后通过实例对模型检测过程进行了详细说明，本文的研究成果有效地说明了将模型检测应用于森林防火专家系统等林业信息系统的可行性与正确性。

关键词：模型检测；知识库模型；状态迁移图；时序逻辑

中图分类号：TP311 文献标识码：A 文章编号：2095-2163（2014）02-

The Research of Model Checking Application Method for

Forestry Information System

WU Di，JI Mingyu，TAN Keshan，WANG Hui，ZHANG Jin

（College of Information and Computer Engineering，Northeast Forestry University， Harbin 150040，China）

Abstract： As a formal verification technique， model checking has been successfully applied in the property verification process of hardware and protocol and is turning to the field of software verification and gradually expanded its scope of application. Aiming to the knowledge base of expert system for forest fire prevention rules， the paper researches the formal verification problems for properties specification to be satisfied. Fist， the rule body is described as state transition graph and the state transition process and state properties of graphs are effectively illustrated by introducing the transfer function. Then the corresponding temporal logic expression for the properties specification is described. Finally， the model checking process is detailed described. The research results of this paper illustrate the feasibility and the correctness and prove that model checking can be applied to the forest fire prevention expert system and other forest information systems a certain extent.

Key words： Model Checking； Knowledge Base Model； State Transition Graph； Temporal Logic

0 引 言

如今，随着社会对软件需求的不断增加，软件设计的复杂度日渐提高，软件测试也日趋困难。与其相应地，模型检测作为一种形式化验证技术，因其自动化程度高并能够自动提供性质反例信息等优点而在软件验证领域引起人们的广泛关注[1]。

信息化的今天，各种数字化林业系统应用广泛，已然在森林资源调查、森林病虫害检测及防治、森林火灾监测和动态管理等方面发挥着重大作用，并在节省了大量的人力物力的同时，实现了对林场的自动化、专业化、高效化和实时化的管理。但在此过程中，也对林业系统的可靠性和安全性却也提出了与以往相比更高的要求，除了对硬件方面的改造升级，如何测试发现系统的潜在错误状态并及时改正则显得尤为重要，模型检测即提供了一个严密，高效的验证手段。……