基于層次組合抽象的智能系統(tǒng)形式化驗證*

周益龍 韓 斌

（江蘇科技大學計算機學院 鎮(zhèn)江 212001）

1 引言

智能系統(tǒng)是將信息技術和嵌入式技術融為一體，實現(xiàn)智能控制的系統(tǒng)。隨著軟硬件規(guī)模的不斷擴大，系統(tǒng)呈現(xiàn)出高并發(fā)的特點，急需一種全面有效的方法保證系統(tǒng)的安全性。

與傳統(tǒng)的仿真和測試技術相比，形式化方法基于嚴格的數(shù)學理論，能夠準確地描述系統(tǒng)模型并進行驗證，具有高可信度的特點。因此，形式化方法已經(jīng)被大量運用于軟硬件系統(tǒng)的設計與開發(fā)中。文獻［1］中，張杰等利用結構建模法對硬件電路形式化建模，并通過定理證明完成了驗證；文獻［2］中，Jin Song Dong等利用形式化語言TCOZ，描述物聯(lián)網(wǎng)系統(tǒng)中的傳感器感知模式、通信行為以及實時約束，通過定理證明的方式完成了模型的手動檢驗；文獻［3］中，Chen等針對無線傳感網(wǎng)絡和無線體域網(wǎng)絡這兩個新型網(wǎng)絡，提出了對其安全協(xié)議形式化驗證的方法；文獻［4］中，Sanghyun Yoon等提出了一種用于混成系統(tǒng)的驗證技術，實現(xiàn)了利用SpaceEx來驗證ECML模型以及搭建了混成系統(tǒng)的驗證平臺；文獻［5］中，閆培等針對生命攸關的智能居家護理系統(tǒng)，提出了形式化建模的框架，利用PAT平臺對模型進行了驗證，找到設計缺陷并進行了改進。

本文針對智能系統(tǒng)提出了一種形式化建模與驗證的方法，旨在發(fā)現(xiàn)系統(tǒng)設計中的缺陷，并以能源共享系統(tǒng)為例對建模過程，最后通過實驗證明了該方法的有效性。

2 形式化方法

形式化方法（FormalMethod）基于嚴格的數(shù)學理論，常被用于計算機軟硬件系統(tǒng)的設計與驗證，其嚴謹?shù)奶攸c能夠有效保證系統(tǒng)的安全性、可靠性等。與傳統(tǒng)的仿真和測試方法相比，形式化方法在減少人力和時間投入的同時，能夠準確清晰地對系統(tǒng)進行描述和驗證，因此，形式化方法已經(jīng)在多個領域中得到了廣泛的應用，特別是安全苛求的系統(tǒng)。

其中，形式化規(guī)約和形式化驗證是形式化方法研究的兩項重要內(nèi)容，如圖1所示。

圖1 形式化方法研究內(nèi)容

形式化規(guī)約過程中，系統(tǒng)模型規(guī)約可以表述為系統(tǒng)的行為建模，系統(tǒng)屬性規(guī)約可以表述為對系統(tǒng)需要滿足的性質建模。通過對系統(tǒng)進行形式化規(guī)約后，可以形式化地驗證系統(tǒng)是否需滿足相應的性質，其中，模型檢測是檢測有限狀態(tài)系統(tǒng)是否滿足期望性質的一項技術，檢測過程完全自動且高效。基本方式是通過對系統(tǒng)狀態(tài)空間的暴力搜索，來搜尋是否存在不符合性質的情況，若存在，將會給出對應的反例路徑，通過反例對系統(tǒng)設計進行分析和修改。

3 層次組合抽象模型

3.1 層次K ripke結構

定義1（層次Kripke結構）層次的Kripke結構可以表示為一個五元組（S，S0，AP，R，L），其中：

1）S表示系統(tǒng)所有狀態(tài)的有限集合；

2）S0∈S表示系統(tǒng)初始狀態(tài)的集合；

3）AP表示原子命題的集合，主要包括了該狀態(tài)下的系統(tǒng)發(fā)生的動作行為；

將能源共享系統(tǒng)劃分為應用層、系統(tǒng)層以及設備層，從應用層由上而下構建各層的Kripke結構，結果可以用帶標簽的有向圖來表示，分別如圖2、圖3、圖4所示。

圖2 應用層模型

圖3 系統(tǒng)層模型

圖4 設備層模型

其中，每個橢圓表示系統(tǒng)的一個狀態(tài)，圈內(nèi)的原子命題表示系統(tǒng)的行為，有向曲線表示系統(tǒng)狀態(tài)的轉移關系。

3.2 組合抽象模型

為了得到簡潔的系統(tǒng)模型，需要利用各個層次之間的相互聯(lián)系，按照正確的組合規(guī)則，將層次Kripke結構模型進行組合建模，現(xiàn)定義層次Kripke結構的組合方式如定義2所示。

圖5 系統(tǒng)組合模型

組合層次Kripke結構模型后，得到的系統(tǒng)組合模型狀態(tài)數(shù)量非常多，模型十分冗雜，其中包含了許多對驗證系統(tǒng)性質并無影響的狀態(tài)，以及一些具有相似行為、可以融合的狀態(tài)。因此，需要對系統(tǒng)的組合模型進行進一步的抽象處理，以達到精簡系統(tǒng)模型的效果。

4）Ra，在抽象狀態(tài)之間重新定義的轉移關系，滿足與之分別對應，并使得成立；

5）La，抽象狀態(tài)的標記函數(shù)。

在對系統(tǒng)組合模型進行抽象時，去除不影響驗證性質的狀態(tài)，將行為相似、位于同一動作序列且無分支的狀態(tài)進行合并；去除抽象狀態(tài)之內(nèi)的轉移關系，并在新的抽象狀態(tài)之間建立新的轉移關系；重新定義抽象狀態(tài)的標記函數(shù)。最終得到系統(tǒng)的組合抽象模型，如圖 6 所示。

圖6 系統(tǒng)組合抽象模型

3.3 組合抽象驗證策略

組合抽象模型的驗證策略可以分為簡單組合策略和假設/保證（A/G）組合策略，在能源共享系統(tǒng)中，每個層次模塊之間存在著相互制約的關系，采用簡單組合策略時會忽略模塊之間的相互影響，與實際情況不符合，因此，本文采用A/G組合策略來對系統(tǒng)模型進行檢測。

A/G組合策略的基本模式如式（1）所示，為驗證M1和M2的并發(fā)組合系統(tǒng)M 滿足性質α和β，需要驗證M1在任意環(huán)境下，滿足性質α；在滿足性質α的環(huán)境下，驗證M2滿足性質β即可。

本文對能源共享系統(tǒng)進行驗證時，采用線性時序邏輯對性質進行描述。對于給定的LTL公式φ和ψ，只需檢測M1|=φ是否成立，就能很容易驗證形如 ＜ture＞Ma＜α＞ 是否成立；而要驗證形如＜α＞M2＜β＞是否成立，根據(jù)文獻［6］中的定理，對于給定的LTL公式φ和ψ，如果φ和ψ中出現(xiàn)的所有原子命題都在M的原子命題集中，那么＜φ＞M2＜ψ＞成立當且僅當M2|=φ→ψ，得到LTL公式的驗證形式如式（2）所示。

在驗證組合抽象模型是否滿足性質時，需要根據(jù)組合模型和抽象模型的原子命題集之間的抽象對應關系，將LTL性質公式中的相關狀態(tài)子公式進行等價的替換，如式（3）所示：

其中，p是LTL公式φ的狀態(tài)子公式，α表示抽象映射，α(p)表示對狀態(tài)子公式 p進行抽象映射以達到等價替換的效果。

然后，結合A/G組合驗證策略，分別驗證各個子系統(tǒng)的抽象性質，從而推斷層次組合抽象系統(tǒng)的整體性質，組合抽象驗證策略如式（4）所示：

4 實驗驗證結果分析

實驗采用CSP#語言對能源共享系統(tǒng)模型進行形式化規(guī)約，得到模型狀態(tài)圖如圖7所示。

圖7 系統(tǒng)層次組合抽象模型狀態(tài)圖

抽取系統(tǒng)的安全性和活性進行LTL斷言設計，其中，系統(tǒng)安全性包括了無死鎖性和無沖突性，系統(tǒng)活性包括了可用性和節(jié)能性（設備開啟后最終會關閉），性質申明分別表述為

1）無死鎖性。系統(tǒng)不會一直處于停滯或等待的狀態(tài)，死鎖起因大多是進程間的相互等待。

2）無沖突性。一位用戶使用的設備數(shù)量總是小于2，一臺設備的使用者數(shù)量總是小于2。

3）可用性。用戶在成功登錄后，總是能夠正常地使用各項功能。

4）節(jié)能性。用戶在使用的過程中，設備最終都需要被關閉。

用進程分析工具PAT完成模型的自動驗證，能源共享系統(tǒng)的性質驗證結果如表1所示。

表1 系統(tǒng)性質驗證結果

分析PAT工具給出的反例路徑可以發(fā)現(xiàn)，1）系統(tǒng)沖突性主要原因是：不同用戶登錄成功后，同時通過掃碼或者輸入編碼的方式獲取同一臺設備的信息，此時，如果這些用戶未租借其他設備，而此設備也空閑，滿足租賃條件，那么這些用戶能夠同時發(fā)起開啟設備的請求，引發(fā)沖突。解決方案：在用戶掃碼或者輸入編碼后查看設備信息的同時，系統(tǒng)對該設備進行鎖定，如果用戶一定時間內(nèi)未進行相關操作，系統(tǒng)就解鎖該設備。2）系統(tǒng)不滿足節(jié)能性的主要原因是：用戶在租借設備后，可能進行了諸多其他無關操作，從而忘記了關閉正在使用中的設備，導致設備無限長時間內(nèi)一直處于使用中狀態(tài)，造成能源浪費。解決方案：用戶租用設備后，系統(tǒng)在界面醒目位置顯示結束使用的功能，并在一定時間后提醒用戶關閉設備，如果用戶長時間未關閉設備，系統(tǒng)自動關閉設備，結束租用。

使用抽象模型、組合模型和層次組合抽象模型分別對能源共享系統(tǒng)進行建模，用PAT進行驗證后得到系統(tǒng)狀態(tài)數(shù)隨用戶數(shù)量變化的對比圖，如圖8所示。

圖8 結果對比圖

通過狀態(tài)數(shù)的對比實驗可以得出，層次組合抽象模型既能夠有效減少系統(tǒng)模型中的狀態(tài)基數(shù)，也能減緩系統(tǒng)狀態(tài)數(shù)隨系統(tǒng)并發(fā)量增長的速度，在一定程度上緩解了模型檢測中的狀態(tài)空間爆照問題，使得模型檢測工作能夠更加有效率地進行。

5 結語

本文結合了層次Kripke結構和組合抽象技術，提出了利用層次組合抽象模型對智能系統(tǒng)進行形式化驗證的方法，通過實例驗證，證明該方法能夠準確找出系統(tǒng)設計缺陷，并能有效緩解狀態(tài)空間爆炸問題，提高模型檢測的效率。