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

周益龍 韓 斌

（江蘇科技大學(xué)計(jì)算機(jī)學(xué)院 鎮(zhèn)江 212001）

1 引言

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

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

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

2 形式化方法

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

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

圖1 形式化方法研究?jī)?nèi)容

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

3 層次組合抽象模型

3.1 層次K ripke結(jié)構(gòu)

定義1（層次Kripke結(jié)構(gòu)）層次的Kripke結(jié)構(gòu)可以表示為一個(gè)五元組（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ā)生的動(dòng)作行為；

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

圖2 應(yīng)用層模型

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

圖4 設(shè)備層模型

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

3.2 組合抽象模型

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

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

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

4）Ra，在抽象狀態(tài)之間重新定義的轉(zhuǎn)移關(guān)系，滿足與之分別對(duì)應(yīng)，并使得成立；

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

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

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

3.3 組合抽象驗(yàn)證策略

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

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

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

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

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

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

4 實(shí)驗(yàn)驗(yàn)證結(jié)果分析

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

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

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

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

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

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

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

用進(jìn)程分析工具PAT完成模型的自動(dòng)驗(yàn)證，能源共享系統(tǒng)的性質(zhì)驗(yàn)證結(jié)果如表1所示。

表1 系統(tǒng)性質(zhì)驗(yàn)證結(jié)果

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

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

圖8 結(jié)果對(duì)比圖

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

5 結(jié)語

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