唐敏 吳熊 李平 唐晨 楊國(guó)榮

摘 要：對(duì)混成系統(tǒng)進(jìn)行安全性驗(yàn)證是計(jì)算機(jī)領(lǐng)域具有重要意義和挑戰(zhàn)性的課題，傳統(tǒng)的測(cè)試仿真技術(shù)不足以確保系統(tǒng)的絕對(duì)安全性和完備性?；谛问交椒ㄊ歉鶕?jù)混成系統(tǒng)的形式規(guī)范與屬性，使用數(shù)學(xué)方法證明其正確性或非正確性。對(duì)溫控系統(tǒng)實(shí)現(xiàn)了抽象算法的形式化，首先對(duì)線性混成系統(tǒng)的狀態(tài)空間進(jìn)行分割，然后將其轉(zhuǎn)化為圖的可達(dá)性問(wèn)題，利用圖算法求解，最終對(duì)系統(tǒng)進(jìn)行了安全性驗(yàn)證。實(shí)驗(yàn)結(jié)果表明，采用形式化方法對(duì)混成系統(tǒng)進(jìn)行安全性驗(yàn)證具有較高的可靠性與可信性。

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

DOI：10.11907/rjdk.172346

中圖分類號(hào)：TP301

文獻(xiàn)標(biāo)識(shí)碼：A 文章編號(hào)：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)相互作用而構(gòu)成的一類動(dòng)態(tài)系統(tǒng)。連續(xù)變量系統(tǒng)的動(dòng)態(tài)特征隨時(shí)間推移在不斷演化，離散事件系統(tǒng)的動(dòng)態(tài)演化則受事件的驅(qū)動(dòng)，兩者相互作用使系統(tǒng)表現(xiàn)出更加復(fù)雜的動(dòng)態(tài)行為[1]。以統(tǒng)一化、一般化的模式對(duì)混成系統(tǒng)進(jìn)行深入研究，形成了當(dāng)今控制科學(xué)與計(jì)算機(jī)科學(xué)界的前沿?zé)狳c(diǎn)。一般來(lái)說(shuō)，保障軟件質(zhì)量與系統(tǒng)穩(wěn)定的主要方法可以采用測(cè)試和仿真，但傳統(tǒng)的測(cè)試仿真[2]不足以確保系統(tǒng)的絕對(duì)安全性和完備性[3]，模型檢測(cè)[4]與演繹推理[5]適用于有限狀態(tài)空間的系統(tǒng)，對(duì)于無(wú)限狀態(tài)的混成系統(tǒng)，不能覆蓋其全部狀態(tài)空間。形式化方法則是基于數(shù)學(xué)基礎(chǔ)，對(duì)系統(tǒng)進(jìn)行說(shuō)明、設(shè)計(jì)及驗(yàn)證，包括語(yǔ)言、技術(shù)與工具[6，7]。本文基于形式化驗(yàn)證理論，結(jié)合形式化技術(shù)對(duì)混成系統(tǒng)模型的可達(dá)性及安全性驗(yàn)證進(jìn)行研究，并將形式化方法具體應(yīng)用到溫控系統(tǒng)中。

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

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

2 基于抽象形式化驗(yàn)證方法

由于混成系統(tǒng)復(fù)雜性高，可達(dá)狀態(tài)可能是無(wú)窮的，導(dǎo)致從初始狀態(tài)集計(jì)算所有可達(dá)狀態(tài)變得困難甚至不可能。利用抽象來(lái)減少?gòu)?fù)雜度，通過(guò)對(duì)狀態(tài)空間進(jìn)行分割，將混成系統(tǒng)分成多個(gè)有限的狀態(tài)空間，然后將混成系統(tǒng)的安全性驗(yàn)證問(wèn)題轉(zhuǎn)換為圖的可達(dá)性分析問(wèn)題進(jìn)行驗(yàn)證。

2.1 相關(guān)概念

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

2.2 抽象算法

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

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

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

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

2.2.2 抽象函數(shù)

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

c2.2.3 抽象算法

由2.2.1中得到的每一塊區(qū)域作為有向圖的頂點(diǎn)，將2.2.2中抽象函數(shù)轉(zhuǎn)化為有向圖的邊，實(shí)際研究?jī)?nèi)容轉(zhuǎn)變?yōu)榻鉀Q圖的可達(dá)性問(wèn)題。采用深度優(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（）；

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

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

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

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

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

3 結(jié)語(yǔ)

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

參考文獻(xiàn)：

[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)導(dǎo)論CPS方法[M].北京：機(jī)械工業(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歸納構(gòu)造演算的藝術(shù)[M].北京：清華大學(xué)出版社，2010.

[9] 李倩.基于形式化方法的混成系統(tǒng)安全性驗(yàn)證[D].上海：華東師范大學(xué)，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.

（責(zé)任編輯：劉亭亭）