林业信息系统模型检测应用方法研究

吴迪

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

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

中图分类号：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]。

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

1 模型检测

模型检验[2]以穷尽搜索为基础，通过对软件系统或系统的某一部分建模，利用某种形式化方法说明系统应满足的属性，以此来判断软件系统是否满足这些期望的属性。模型检测的一般流程是：首先将待检测的系统抽象建模为状态迁移图（不同的状态通过状态变量取值加以区分），然后使用时序逻辑表达式描述待验证的系统性质，进而通过模型检测工具完成系统性质的自动验证[3，4，5]。模型检测流程如图1所示。

图1 模型检测流程

Fig.1 Model checking process

2 林业信息系统分析

林业信息系统的应用涉及林业管理的多个方面，本文主要以林火子系统中森林防火专家系统性质验证问题为切入点进行形式化验证分析。森林防火专家系统由知识库、推理机、解释模块和知识获取等部分组成[6]，其系统结构如图2所示。

图2 森林防火专家系统结构图

Fig.2 The structure diagram of forest fire prevention expert system

通过对系统结构分析可知，系统建立的重点在于对知识库的构建。下文主要针对森林防火专家系统的部分系统规则，对具体的验证过程展开分析。

3模型检测过程

森林防火专家系统的模型检测过程主要为：对森林防火专家系统进行抽象建模，得出具体的状态迁移图；通过时序逻辑表达式描述森林防火系统的重要功能需求；应用具体模型检测器进行性质验证[7，8]。

通过对森林专家防火系统的知识库进行分析可知，专家系统的知识库主要是应用了“规则架+规则体”的形式，即知识库中的每条规则都有一个规则架，每个规则架对应一个或多个规则体，并且每条规则架或规则体都是多个前提一个结论的结构（如：if 火焰高度，火速 then 扑火方式）。

森林防火系统中的林火状态可分为正常状态，防火预测，火灾处理，火后状态等多个分类状态。每个分类状态又是由不同的子状态组成的。各子状态之间通过状态迁移进行联系。

森林防火专家系统的状态迁移过程需满足如下待验证规范：

（1） 每个规则架或规则体都是对应的多个前提和一个结论（即不存在不符合规则体的状态）；

（2） 不存在多个前提多个结论的状态（即不存在不符合规则体的状态）；

（3） 无论什么状态最终都会迁移到某个特定状态（如所有分类状态最终会达到正常状态）；

（4） 不存在某几个变量同时为真的状态（如火焰高度大于2m，风速较大时不能采用飞机喷洒这种间接扑火方式）；

（5） if变量组合只能与特定then变量同时为真的状态等。

4实例分析

本文将多个规则体中的前提和结论看成系统的状态变量，从而抽象出迁移系统模型，并设置系统的入口，以便进行性质验证。

下面对知识库部分规则体进行说明如下：

（1） if 无火源 适当湿度 温度 降水量 then正常状态

（2） if 林中可燃物湿度>60℃ hen 林区不会发生火灾

（3） if 林区被积雪覆盖 then 一定不会发生火灾

（4） if 某区域出现红外线光长>=3.7微米 then 该区域一定有火源

（5） if 林火区出现高空逆温层 then 林火影响因子不大

（6） if 林火区出现快性冷锋 then 林火影响因子很大

（7） if 发生火灾 坡度 风速 then 火焰蔓延速度 火焰蔓延速度=F（坡度， 风速， 可燃物湿度）

（8） if 火焰高度<2m 火速<20m/min then 直接扑火方式；

（9） if 直接扑火状态 then 扑火方式为人工扑火

（10） if 火焰高度>=2m 火速>=20m/min then 间接扑火方式；

（11） if 间接扑火状态 风速较小 then 扑火方式为飞机喷洒

（12） if 间接扑火状态 风速较大 then 扑火方式为隔离带

（13） if 火后无明火 湿度较小 then 需要二次扑火

（14） if 火后无明火 湿度较大 then 无需二次扑火

其正常状态为状态（1）；防火预测状态为状态（2）（3）（4）（5）（6）；火灾处理状态为状态（7）（8）（9）（10）（11）（12）；火后处理状态为状态（13）（14）。

上述规则体中可抽象出状态迁移变量如表1所示。

图3 状态迁移图

Fig.3 State transition diagram

对于系统的状态迁移图，待验证的性质为：每一个有火源的状态必然存在一条以上的迁移路径，使其到达火后处理状态。对于这条性质可采用计算树逻辑[9，10]对其进行描述。具体的逻辑表达式为 。

对于系统状态变迁过程中的状态变量描述，本文对系统中涉及的数值类型迁移变量进行了规范化处理，通过变换函数的方法在保证其意义不变的情况下将数值域状态变量转化为布尔域变量，相应的数值类型迁移变量如表2所示。

变换函数为 ，其中参数 代表数值型数据的值，参数 表示当前状态所处的分类状态（正常状态、防火预测、火灾处理、火后处理），不同状态下临界值不相同，若 临界值，则 ，否则 。通过上述变换函数处理后，即可得到数值型数据的布尔型数值。

最后，基于上述状态迁移图及性质描述，作者通过相应的模型检测工具完成了性质的验证，关于模型检测工具的使用不是本文的重点研究内容，在此就不作赘述了。

5结束语

本文将模型检测技术应用到林业信息系统性质验证，针对森林防火专家系统提出了模型检测状态迁移图表示方法，并给出具体的验证过程说明，下一步笔者将更进一步对模型检测算法的设计和优化细节进行深入研究。

参考文献：

[1] 林惠民，张文辉. 模型检测：理论，方法与应用[J]. 电子学报，2002，30（12）：1907-1912.

[2] 王飞明，胡元闯，董荣胜. 模型检测研究进展[J]. 广西科学院学报.2008，24（4）：320-328.

[3] 顾滨兵. 一种软件模型检测方法及其原型系统[J]. 微计算机，2010，31（11）：39-40.

[4] 张宁宁，刘孟仁. 模型检测在软件测试中的应用[J]. 计算机与数字，2006，34（2）：93-96.

[5] 袁志斌，徐正权，王能超. 软件模型检测中的抽象[J]. 计算机科学，2006，33（7）：276-279.

[6] 王阿川，曹琳，冯艳红. 基于网络的森林防火专家系统实现技术[J]. 东北林业大学学报，2006，34（1）：109-110.

[7] 肖健宇，张德运，郑卫斌，张勇. 程序条件化用于软件模型检测中的状态空间缩减[J]. 西安交通大学学报，2006，40（4）：377-380.

[8] 黎吾平. 模型检测在软件方面的应用[D]. 吉林大学硕士论文. 2008.4.

[9] 周从华，刘志锋，王昌达. 概率计算树逻辑的界限模型检测[J]. 软件学报，2012，23（7）：1657-1668.

[10] 黄宏涛. 基于惰性切片的模型检测技术研究[D]. 哈尔滨工程大学硕士论文. 2004.6.