林業信息系統模型檢測應用方法研究

吳迪

摘 要：模型檢測作為一種形式化驗證技術已成功應用于硬件以及協議的性質驗證過程，目前正轉向軟件驗證領域并逐漸擴展其應用范圍。針對特定的森林防火專家系統的知識庫規則，研究其所需滿足的性質規范的形式化驗證問題。首先將規則體描述為狀態遷移圖，通過引入轉換函數對狀態遷移圖的變遷過程及狀態性質進行了有效說明，然后將性質規范描述為相應的時序邏輯表達式，最后通過實例對模型檢測過程進行了詳細說明，本文的研究成果有效地說明了將模型檢測應用于森林防火專家系統等林業信息系統的可行性與正確性。

關鍵詞：模型檢測；知識庫模型；狀態遷移圖；時序邏輯

中圖分類號：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.