基于形式化方法的混成系統(tǒng)驗證

唐敏 吳熊 李平 唐晨 楊國榮

摘 要：對混成系統(tǒng)進行安全性驗證是計算機領域具有重要意義和挑戰(zhàn)性的課題，傳統(tǒng)的測試仿真技術不足以確保系統(tǒng)的絕對安全性和完備性。基于形式化方法是根據(jù)混成系統(tǒng)的形式規(guī)范與屬性，使用數(shù)學方法證明其正確性或非正確性。對溫控系統(tǒng)實現(xiàn)了抽象算法的形式化，首先對線性混成系統(tǒng)的狀態(tài)空間進行分割，然后將其轉化為圖的可達性問題，利用圖算法求解，最終對系統(tǒng)進行了安全性驗證。實驗結果表明，采用形式化方法對混成系統(tǒng)進行安全性驗證具有較高的可靠性與可信性。

關鍵詞：形式化方法；抽象算法；混成系統(tǒng)；溫控系統(tǒng)

DOI：10.11907/rjdk.172346

中圖分類號：TP301

文獻標識碼：A 文章編號：1672-7800（2018）004-0039-03

Abstract：The safety verification of hybrid systems is an important and challenging subject in the computer field. The traditional test and simulation technology is not enough to ensure the absolute security and completeness of the system. The formal verification method is based on the formal specification of hybrid systems and properties， using mathematical method to testify its correctness. We implement the formalization of the abstraction algorithm to verify the safety of temperature control systems. We first divide the state space of a linear hybrid system into several parts， and then transform it to the reachability problem of a graph， finally we use graph algorithm to verify the safety of this system. Compared with the simulation and testing methods， the formal method has higher reliability and credibility.

Key Words：formal methods； abstract algorithms； hybrid systems； temperature control systems

0 引言

混成系統(tǒng)是由連續(xù)變量系統(tǒng)和離散事件系統(tǒng)相互作用而構成的一類動態(tài)系統(tǒng)。連續(xù)變量系統(tǒng)的動態(tài)特征隨時間推移在不斷演化，離散事件系統(tǒng)的動態(tài)演化則受事件的驅(qū)動，兩者相互作用使系統(tǒng)表現(xiàn)出更加復雜的動態(tài)行為[1]。以統(tǒng)一化、一般化的模式對混成系統(tǒng)進行深入研究，形成了當今控制科學與計算機科學界的前沿熱點。一般來說，保障軟件質(zhì)量與系統(tǒng)穩(wěn)定的主要方法可以采用測試和仿真，但傳統(tǒng)的測試仿真[2]不足以確保系統(tǒng)的絕對安全性和完備性[3]，模型檢測[4]與演繹推理[5]適用于有限狀態(tài)空間的系統(tǒng)，對于無限狀態(tài)的混成系統(tǒng)，不能覆蓋其全部狀態(tài)空間。形式化方法則是基于數(shù)學基礎，對系統(tǒng)進行說明、設計及驗證，包括語言、技術與工具[6，7]。本文基于形式化驗證理論，結合形式化技術對混成系統(tǒng)模型的可達性及安全性驗證進行研究，并將形式化方法具體應用到溫控系統(tǒng)中。

1 混成系統(tǒng)形式化定義

令房間初始溫度為20℃，加熱器處于關閉狀態(tài)，初始狀態(tài)為（loff，x0），x0=20，c=0。從安全性上描述該系統(tǒng)，在加熱器工作期間，能夠確保房間內(nèi)的溫度保持在安全區(qū)域，保證溫度處在最低溫度與最高溫度范圍內(nèi)。

2 基于抽象形式化驗證方法

由于混成系統(tǒng)復雜性高，可達狀態(tài)可能是無窮的，導致從初始狀態(tài)集計算所有可達狀態(tài)變得困難甚至不可能。利用抽象來減少復雜度，通過對狀態(tài)空間進行分割，將混成系統(tǒng)分成多個有限的狀態(tài)空間，然后將混成系統(tǒng)的安全性驗證問題轉換為圖的可達性分析問題進行驗證。

2.1 相關概念

為了進一步說明抽象方法的思想，引入混成系統(tǒng)的幾個重要概念。

2.2 抽象算法

抽象算法[9]的關鍵在于抽象狀態(tài)的安全性與混成系統(tǒng)實際的狀態(tài)空間安全性直接的對應關系。抽象算法的基本步驟為：①抽象化混成系統(tǒng)的狀態(tài)空間；②利用有效轉換，把混成系統(tǒng)的安全性問題轉化為圖的可達性分析問題；③利用圖算法對其進行求解。以恒溫器為例闡述抽象算法的實現(xiàn)。

假設一個恒溫系統(tǒng)具有3種工作狀態(tài)：①Heat：加熱；②Cool：制冷；③Check：在不加熱不制冷的狀態(tài)下自我檢查。恒溫器的連續(xù)狀態(tài)空間有兩個變量：①環(huán)境溫度，用T表示；②內(nèi)部時鐘，用c表示。使用不變式謂詞描述每個工作狀態(tài)所允許連續(xù)變量值的范圍。恒溫器系統(tǒng)模型如圖2所示。

2.2.1 抽象狀態(tài)空間

有幾種方法來抽象狀態(tài)空間，它可以將狀態(tài)空間抽象為多面體，或?qū)顟B(tài)空間抽象為網(wǎng)格。混成系統(tǒng)行為比較普遍復雜，導致抽象算法主要停留在啟發(fā)式階段。狀態(tài)空間的抽象算法包含3個部分：守衛(wèi)函數(shù)、重置函數(shù)和邊界值。把恒溫器系統(tǒng)在Heat位置時的狀態(tài)空間進行分割，如圖3所示，灰色區(qū)域顯示的是在Heat狀態(tài)下不定式的不可達區(qū)域。

2.2.2 抽象函數(shù)

抽象函數(shù)指系統(tǒng)允許抽象的離散或者連續(xù)轉換[9]。采用overestimate技術描述，用多個轉換來代替系統(tǒng)原有的轉換→ACD，但是要確保初始狀態(tài)等于最終狀態(tài)，如圖4所示。恒溫器系統(tǒng)在區(qū)間[0.5，1）×[5，6）中，所有可能的抽象轉換用箭頭描述。

c2.2.3 抽象算法

由2.2.1中得到的每一塊區(qū)域作為有向圖的頂點，將2.2.2中抽象函數(shù)轉化為有向圖的邊，實際研究內(nèi)容轉變?yōu)榻鉀Q圖的可達性問題。采用深度優(yōu)先算法，流程描述如下：

hash_map=new Hash_map（）；

while hash_map->T ！=null do

stack=new Stack（）；

（l，b）=hash_map.pop（T）；

Stack.push（（l，b））；

while（！stack.isEmpty（））

if==null return stack；

if stack.top（）！=null

（l，b）=stack.top（）；

stack.push（（l，b））；

else if stack.top（hash_map->PostC）！=null

（l，b）=stack.top（hash_map->PostC）；

stack.push（（l，b））；

else stack.pop（）；

算法描述如下：設哈希表hash_mapA存放所有待訪問的狀態(tài)，hash_mapB存放所有已經(jīng)訪問過的狀態(tài)。

（1）選取初始狀態(tài)集的一個點作為初始狀態(tài)，將其放入hash_mapA中。

（2）如果hash_mapB的集合小于狀態(tài)空間，就取hash_mapA中的一個狀態(tài)（l，b）放入棧里面。如果棧頂不為null，循環(huán)做以下操作：①檢查棧頂元素（l，b）是否滿足安全條件，滿足取其元素，不滿足跳出循環(huán)；②檢查是否訪問過（l，b）的離散后繼。如果未訪問，取其全部離散后繼放入hash_mapA；③檢查是否訪問過（l，b）的連續(xù)后繼。如果未訪問，取其全部連續(xù)后繼放入hash_mapA；④否則，將狀態(tài)（l，b）放入hash_mapB。

（3）如果棧為空，表明系統(tǒng)安全；否則說明系統(tǒng)存在狀態(tài)的可達狀態(tài)為不安全區(qū)域，系統(tǒng)不安全。

抽象算法是形式化驗證研究的一種新方法，以恒溫器作為實例，研究得出恒溫器系統(tǒng)在Heat狀態(tài)下的安全性驗證形式化抽象算法。Heat狀態(tài)下的抽象狀態(tài)空間由圖3決定，在該狀態(tài)空間中，隨機抽取下面兩組狀態(tài)集作為待檢測狀態(tài)（狀態(tài)僅檢測T）：{2.5，4.5，3.6，8.7，2.2}和{5.6，4.5，10.6，7.6，3.8}，分別代入上述算法的具體實現(xiàn)中，驗證結果如下：“可達狀態(tài)空間不存在不安全區(qū)域”和“可達狀態(tài)空間存在不安全區(qū)域”。

3 結語

驗證混成系統(tǒng)的安全性是十分困難的問題，傳統(tǒng)算法難以判定[10]。抽象方法降低了問題的復雜度，把系統(tǒng)的狀態(tài)空間映射到抽象狀態(tài)集，同時確保系統(tǒng)的行為保持一致性。混成系統(tǒng)有多種抽象方式，如連續(xù)系統(tǒng)可以被抽象成離散系統(tǒng)；非線性系統(tǒng)可以被抽象成線性系統(tǒng)等。本文基于形式化方法，根據(jù)混成系統(tǒng)的形式規(guī)范和屬性，并結合抽象方法，對混成系統(tǒng)的安全性進行驗證，使用數(shù)學的方法證明其正確性或非正確性。與仿真、程序測試方式相比，形式化方法具有更高可靠性與可信性。

參考文獻：

[1] SCHAFT A， SCHUMACHER J M. An introduction to hybrid dynamical systems[M]. Beijing： Tsinghua University press，2007.

[2] GLOVER W， LYGEROS J. A stochastic hybrid model for air traffic control simulation[J]. Hybrid Systems： Computation and Control. Heidelberg： Springer-Verlag，2004：372-386.

[3] 古天龍.軟件開發(fā)的形式化方法[M].北京：高等教育出版社，2005.

[4] EDMUND M C， ORNA G， DORON P. Model checking[M]. Cambridge： MIT Press，2000.

[5] MANNA Z， PNUELI A. Temporal verification of reactive systems[M]. Heidelberg： Springer-Verlag，1995.

[6] LEE E A， SESHIA S A.嵌入式系統(tǒng)導論CPS方法[M].北京：機械工業(yè)出版社，2011.

[7] GEUVERS H， KOPROWSKI A， SYNEK AUTOMATED D， et al. Machine-checked hybrid system safety proofs[M]. Heidelberg： Springer-Verlag，2010.

[8] BERTOT Y， CATERAN P.交互式定義證明與程序開發(fā)——Cop歸納構造演算的藝術[M].北京：清華大學出版社，2010.

[9] 李倩.基于形式化方法的混成系統(tǒng)安全性驗證[D].上海：華東師范大學，2015：12-46.

[10] GULWANI S. Automating string processing in spreadsheets using input-output examples[J]. ACM Sigplan-sigact Symposium on Principles of Programming Languages，2011，46（1）：317-330.

（責任編輯：劉亭亭）