周 穎 段鵬飛 翟小祥 李必信

(東南大學計算機科學與工程學院, 南京 211189)

基于DATL的信息物理融合系統(tǒng)安全性建模與驗證

周 穎 段鵬飛 翟小祥 李必信

(東南大學計算機科學與工程學院, 南京 211189)

為解決微分時態(tài)動態(tài)邏輯(dTL)表達能力弱以及微分代數(shù)動態(tài)邏輯(DAL)缺少時序表達能力的問題,提出了一種結合dTL和DAL的微分代數(shù)動態(tài)時態(tài)邏輯(DATL).采用微分代數(shù)程序(DAP)作為操作模型,使DAL具有dTL的時序處理能力.定義了DATL操作模型的DAP和DATL語法,給出了DAP的跡語義和DATL語義,在繼承dTL和DAL規(guī)則的基礎上新增了6個規(guī)則.通過對飛機避撞系統(tǒng)安全性的規(guī)約和驗證,檢驗了DATL的有效性.

信息物理融合系統(tǒng);屬性驗證;微分時序動態(tài)邏輯;微分代數(shù)動態(tài)邏輯;微分代數(shù)時序動態(tài)邏輯

信息物理融合系統(tǒng)(CPS)將計算和物理過程融合在一起,并通過嵌入式計算機和網(wǎng)絡對物理過程進行監(jiān)控,在監(jiān)控過程中,計算過程和物理過程通過反饋循環(huán)相互影響[1].CPS往往應用于對安全性要求較高的領域,因此保障安全性極為重要.形式化驗證可以檢查系統(tǒng)是否滿足某些屬性,從而發(fā)現(xiàn)系統(tǒng)的設計缺陷,保障系統(tǒng)的安全性.

CPS涉及到離散過程和連續(xù)過程的交互,這點與混成系統(tǒng)類似[2]. CPS具有混成系統(tǒng)的特點,但也有明顯的不同點:CPS由很多自治能力強并且相互間存在協(xié)作的子系統(tǒng)組成,強調子系統(tǒng)之間的協(xié)作和通信;混成系統(tǒng)則更多強調的是一種系統(tǒng)類型的定義, 并不強調通信. Platzer等[3]認為包含離散過程和連續(xù)過程的混成系統(tǒng)可以作為CPS的一個典型數(shù)學模型.王中杰等[4]認為CPS屬于混成系統(tǒng)的研究范疇,混成系統(tǒng)中的許多模型和技術(如離散事件模型、計算智能模型、博弈法等)都可以作為研究CPS時的借鑒.

驗證混成系統(tǒng)的方法主要可分為模型檢驗和推理驗證2類.模型檢驗是一種驗證有窮狀態(tài)系統(tǒng)的技術[5].在模型檢驗方法中,使用時態(tài)邏輯公式對屬性進行規(guī)約,并采用一種有效靈活的搜索步驟,在并發(fā)系統(tǒng)的有限狀態(tài)圖中尋找正確的時態(tài)模式.給定一個有限狀態(tài)模型M、狀態(tài)S以及屬性公式F,對系統(tǒng)屬性的驗證問題轉換為公式M,Sg是否成立的問題.然而,由于混成系統(tǒng)的可達性一般都是不可判定的,而且系統(tǒng)狀態(tài)空間極大,因此需要對系統(tǒng)模型進行各種抽象或者近似處理[6-7]. Alur[8]在《CPS原理》一書中系統(tǒng)闡述了CPS的基本原理以及CPS的建模、測試與驗證.

dTL和DAL是2種形式化的驗證方法,可對CPS進行系統(tǒng)建模、屬性規(guī)約和屬性驗證[9].dTL采用混合程序(hybrid program,HP)作為操作模型,表達能力有限,不能對復雜的CPS進行建模,無法表達物理過程的波動和誤差;而DAL的操作模型DAP通過引入量詞彌補了HP的缺陷.dTL推理驗證方法要求微分方程必須可解,導致dTL只能對具有簡單動態(tài)的CPS進行屬性驗證,無法驗證具有非平凡動態(tài)的CPS屬性;DAL則通過引入微分不變量,解決了非平凡微分方程的求解問題.DAL無法驗證時序屬性, dTL則通過引入時態(tài)操作符并擴充相關的推理規(guī)則,具備了驗證時序屬性的能力.

Zhai等[10]在動態(tài)微分邏輯的基礎上提出了一種建模和驗證CPS的框架,利用混合UML對CPS進行建模,采用微分動態(tài)邏輯對屬性進行抽象和描述,然后驗證CPS模型是否滿足相應的屬性.Xiong等[11]、Lü等[12]、Quaglia[13]研究了CPS的建模和驗證問題,但沒有采用混合UML 和微分動態(tài)邏輯.

本文結合dTL和DAL的優(yōu)點, 提出了一種微分代數(shù)動態(tài)時態(tài)邏輯(DATL),并將其應用于飛機避撞系統(tǒng)的安全性規(guī)約和驗證過程中.

1 基本術語

定義1(混合程序HP)[9]HP是按照如下遞歸定義的最小集合:

1) 如果xi∈Σ為狀態(tài)變量(Σ為狀態(tài)變量、函數(shù)和謂詞關系的集合),并且θi∈Trm(Σ)(1≤i≤n)為項,那么(x1:=θ1,…,xn:=θn)∈HP;

3) 如果χ為一階公式,那么(?χ)∈HP;

4) 如果α,β∈HP,那么(α∪β)∈HP;

5) 如果α,β∈HP,那么(α;β)∈HP;

6) 如果α∈HP,那么(α*)∈HP.

定義2(微分代數(shù)程序DAP)[9]DAP是按照如下遞歸定義的最小集合:

1) 如果J是DJ約束,那么J是DAP;

2) 如果D是DA約束,那么D是DAP;

3) 如果α,β∈DAP,那么(α∪β)∈DAP;

4) 如果α,β∈DAP,那么(α;β)∈DAP;

5) 如果α∈DAP,那么(α*)∈DAP.

定義3(DJ約束)[9,14]DJ約束是按照如下遞歸定義的最小約束條件集合:

1) DJ約束原子公式是DJ約束;

2) 如果A是DJ約束,那么(A)也是DJ約束;

3) 如果A,B是DJ約束,那么(A∧B),(A∨B),(A→B),(A?B)也是DJ約束;

4) 如果A是DJ約束,那么?xA,?xA也是DJ約束;

5) 只有有限次地應用約束條件1～條件4構成的符號串才是DJ約束;

6) 規(guī)定DJ約束中的賦值語句x:=θ不會出現(xiàn)在?x,?x的轄域內.

定義4(DJ約束原子公式)[9,14]DJ約束原子公式是按照如下遞歸定義的最小集合中的元素:

1) 賦值語句x:=θ是DJ約束原子公式,其中x=(x1,x2,…,xn),θ=(θ1,θ2,…,θn),x1,x2,…,xn為個體變項,θ1,θ2,…,θn為項;

2) 設R(x1,x2,…,xn)為n元謂詞符號,t1,t2,…,tn為項,則R(t1,t2,…,tn)是DJ約束原子公式.

定義5(項)[9,14]項是按照如下遞歸定義的最小集合中的元素:

1) 個體常項符號、個體變項符號是項;

2) 若φ(x1,x2,…,xn)是n元函數(shù)符號,t1,t2,…,t3是n個項,則φ(t1,t2,…,tn)是項;

3) 所有項都是有限次使用條件1和條件2得到的.

定義6(DA約束)[9]DA約束是定義在Σ∪Σ′上的一階邏輯公式,其中Σ′為Σ中狀態(tài)變量x的n階導數(shù)x(n)的集合,且Σ′中的符號x(n)不能出現(xiàn)在?x,?x的轄域內.DA約束中的狀態(tài)變量x有可能改變當且僅當DA約束中出現(xiàn)x(n).

2 CPS建模和屬性規(guī)約

2.1 飛機避撞系統(tǒng)

(1)

(2)

如果某一時刻飛機U和飛機V之間的距離小于某值p,則認為這2架飛機存在撞機的危險,應該采取某種策略避免撞機. 將文獻[9]中二維情形下的飛機避撞系統(tǒng)擴展成三維情形下的避撞系統(tǒng).如圖1所示,已知飛機U的坐標(u1,u2,u3),經(jīng)過此點存在唯一平面A與地平面平行;同理,經(jīng)過點(v1,v2,v3)存在唯一平面B與地平面平行. 忽略飛機本身大小,將飛機V投影到平面A上,得到點v′,此時在平面A上一定存在一個圓C1,圓心設為c,三維坐標為(c1,c2,u3),且點u和點v′在圓上.同理,在平面B上,存在一個圓C2,圓心為c′,三維坐標為(c1,c2,v3),且點v在圓上.由此可知,飛機避撞系統(tǒng)可描述為,當飛機U和飛機V的距離小于某值p時,這2架飛機別在平面A和平面B內將各自的飛行方向改變?yōu)閳AC1和圓C2的切線方向,然后,在平面A和平面B內按照如下微分方程描述的動態(tài)飛行一段時間：

圖1 飛機避撞系統(tǒng)

(3)

(4)

為敘述方便,將式(3)簡寫為F(ω,0,0),式(4)簡寫為G(ω,0,0).

由于飛機U和飛機V在整個避撞過程中高度不變,因此式(3)和(4)省略了描述高度的微分方程.避撞過程完畢后,飛機進入自由飛行狀態(tài).如果一段時間后再次遇到撞機危險,則采取同樣的避撞策略.

2.2 DAP的跡語義

由HP建立的模型在隨后的dTL相繼式演算過程中必須是多項式算術內可解的.對于飛機避撞系統(tǒng)而言,飛機在自由飛行時所遵循的微分方程式(1)和(2)在多項式算術內是不可解的,其解是一個超越函數(shù).因此,HP不能對此飛機避撞系統(tǒng)進行建模,也就不能用dTL驗證其屬性.

由DAP建立的模型在相繼式演算的過程中無需求解微分方程.故在DATL中引入DAP作為其操作模型.但是,由于DAP在時序行為下的狀態(tài)變遷語義發(fā)生了變化,故需要定義DAP在時序行為下的狀態(tài)變遷語義——跡語義.

在混合跡定義的基礎上,給出了DAP的跡語義.

定義8(DAP的跡語義) DAPα的跡語義τ(α)是α的所有可能的跡的集合,遞歸地定義如下:

3)τ(α∪β)=τ(α)∪τ(β).

5)τ(α*)=∪n∈Nτ(αn),當n≥1時,αn+1:=(αn;α),且α1:=α,α0:=(?true).

2.3 飛機避撞系統(tǒng)建模

利用DAP對飛機飛行的整個過程進行建模,所建模型為trm*,其中*表示重復執(zhí)行trm.trm包含如下3個階段:自由飛行階段(用free表示)、航向改變階段(假設此階段瞬間完成,不考慮時間延遲,用tang表示)和限制飛行階段(飛機飛行必須滿足動態(tài)F(ω,0,0)∧G(ω,0,0)).令φ表示飛機X和飛機Y的距離大于或等于p,d:=ω(x-c)⊥為d1:=-ω(x2-c2),d2:=ω(x1-c1)的簡寫,e:=ω(y-c)⊥為e1:=-ω(y2-c2),e2:=ω(y1-c1)的簡寫.則有

trm≡free;tang;F(ω,0,0)∧G(ω,0,0)

(5)

(6)

(x3-y3)2≥p2

(7)

tang≡ ?uω:=u;?c(d:=ω(x-c)⊥∧e:=

ω(y-c)⊥)

(8)

2.4 飛機避撞系統(tǒng)安全性規(guī)約

本文需要驗證的屬性是:飛機在任何時刻都是安全的,即飛機在任何時刻都不會發(fā)生碰撞.這個屬性帶有時序特性,任何時刻DAL都無法對這種帶有時序特性的CPS屬性進行規(guī)約.本文使用DATL對飛機避撞系統(tǒng)進行屬性規(guī)約,方法如下: 將安全屬性“飛機在任何時刻都不會發(fā)生碰撞”規(guī)約為DATL公式ψ≡φ→[trm*]φ,即φ成立則[trm*]φ也成立. [trm*]φ成立表示DAP trm*中任意一條執(zhí)行路徑上的所有狀態(tài)下φ都成立.因此,ψ表示如果2架飛機的距離大于等于p,則在trm*執(zhí)行的任意時刻,這2架飛機的距離依然大于等于p.

3 CPS屬性驗證

為了使用DATL的相繼式演算對公式ψ進行推理驗證,在DAP跡語義的基礎上,引入如下6個新規(guī)則:

([;])

([α])

下面利用DATL的相繼式演算來證明公式ψ.演算過程要用到的規(guī)則如下:

T≡d-e=ω(x-y)⊥≡d1-e1=

-ω(x2-y2)∧d2-e2=ω(x1-y1)

??⊥[trm?](true)?⊥[trm?](?ω?ω?x?y?d?e(?→?))?⊥[trm?](free)?[]gen…?⊥[tang](?∧T )…?∧T ⊥[F (ω，0，0)∧G (ω，0，0)]??⊥[tang；F (ω，0，0)∧G (ω，0，0)]??⊥[trm?][free][tang；F (ω，0，0)∧G (ω，0，0)]??⊥[trm?][free][tang][F (ω，0，0)∧G (ω，0，0)]??⊥[trm?][free][tang][F (ω，0，0)∧G (ω，0，0)]□??⊥[trm?][trm]□??⊥[trm?]□?⊥?→[trm?]□?

T′≡ (d1-e1)′=-ω(x2-y2)′∧(d2-e2)′=

ωd1-ωe1=ω(d1-e1)≡true

同理,有

(2(x1-y1)(x1-y1)′+2(x2-y2)(x2-y2)′+

2(x3-y3)(x3-y3)′≥0)F(ω,0,0)∧G(ω,0,0)≡

2(x1-y1)(d1-e1)+2(x2-y2)(d2-e2)+

2(x3-y3)(0-0)≥0≡

2(x1-y1)(d1-e1)+2(x2-y2)(d2-e2)≥0

由于

T≡d-e=ω(x-y)⊥≡d1-e1=

-ω(x2-y2)∧d2-e2=ω(x1-y1)

因此

2(x2-y2)ω(x1-y1)=0≥0≡true

ax∧r??⊥?ax??⊥ω(x-c)┴-ω(y-c)┴=ω(x-y)┴?⊥?∧ω(x-c)┴-ω(y-c)┴=ω(x-y)┴?⊥[d：=ω(x-c)┴∧e：=ω(y-c)┴](?∧T )?⊥?ω?c[d：ω(x-c)┴∧e：=ω(y-c)┴](?∧T )?⊥[tang](?∧T )

圖3 續(xù)圖2中演算過程右分支的左邊部分

r??⊥?α(T′F (ω，0，0)∧G(ω，0，0))?，T ⊥[F (ω，0，0)∧G (ω，0，0)]T DIr??⊥?α(T →?′F (ω，0，0)∧G (ω，0，0))?⊥[F (ω，0，0)∧G (ω，0，0)∧T ]??，T ⊥[F (ω，0，0)∧G (ω，0，0)]??∧T ⊥[F (ω，0，0)∧G (ω，0，0)]?

圖4 續(xù)圖2中演算過程右分支的右邊部分

由此可知,圖4中演算過程的2個分支都以*結束.

上述演算過程驗證了公式ψ≡φ→[trm*]φ的正確性,即驗證了飛機避撞系統(tǒng)的安全性.

如果在演算過程的最后不能以*結束,則說明DATL無法驗證該屬性,即無法得出該屬性滿足與否的結論,需改用其他方法進行驗證.

4 結語

本文基于DAL和dTL的優(yōu)點,使用DAL的操作模型DAP作為DATL的操作模型,并將dTL中的時序表達能力引入DATL.通過對飛機避撞系統(tǒng)進行建模、安全性規(guī)約和驗證,證明了方法的有效性.相比于DAL, DATL在規(guī)約和驗證CPS屬性時可以處理時序行為; 相比于傳統(tǒng)的時序邏輯和dTL, DATL可以對更加復雜的CPS系統(tǒng)進行建模; 相比于二維情形下的飛機避撞系統(tǒng),本文提出了三維情形下的飛行避撞系統(tǒng),并且在規(guī)約和驗證避撞系統(tǒng)安全性時考慮了系統(tǒng)的時序行為.

DATL能夠對大規(guī)模的系統(tǒng)進行屬性驗證,除了本文中提到的飛機避撞系統(tǒng)外,還能對列車控制系統(tǒng)、智能電網(wǎng)系統(tǒng)、汽車自動駕駛系統(tǒng)等進行屬性驗證. 下一步需考慮向DATL中引入其他可能成立的規(guī)則,如規(guī)則[D],〈D〉□,[J],〈J〉□等.

References)

[1]Lee E A. Cyber physical systems: Design challenges[C]//2008 11thIEEEInternationalSymposiumonObjectandComponent-OrientedReal-TimeDistributedComputing(ISORC). Los Angeles,CA,USA, 2008: 363-369. DOI:10.1109/isorc.2008.25.

[2]Beckert B, Schlager S. A sequent calculus for first-order dynamic logic with trace modalities[J].AutomatedReasoning, 2001, 2083: 626-641. DOI:10.1007/3-540-45744-5_51.

[3]Platzer A, Clarke E M. The image computation problem in hybrid systems model checking[C]//InternationalConferenceonHybridSystems:ComputationandControl. Pisa,Italy, 2007: 473-486.

[4]王中杰,謝璐璐.信息物理融合系統(tǒng)研究綜述[J].自動化學報.2011,37(10):1157-1166. Wang Zhongjie, Xie Lulu. Cyber-physical systems: A survey[J].ActaAutomaticaSinica, 2011, 37(10): 1157-1166. (in Chinese)

[5]Clarke E M, Emerson E A, Sifakis J. Model checking[J].LectureNotesinComputerScience, 1997, 164(2): 305-349.

[6]Henzinger T A. The theory of hybrid automata[C]//1996IEEESymposiumonLogicinComputerScience. Los Angeles, CA, USA, 1996: 278-292.

[7]Henzinger T A, Nicollin X, Sifakis J, et al. Symbolic model checking for real-time systems[C]//1992IEEESymposiumonLogicinComputerScience. California, USA, 1992: 394-406. DOI:10.1109/lics.1992.185551.

[8]Alur R.Principlesofcyber-physicalsystems[M]. Cambridge, Massachusetts,USA: MIT Press, 2015: 76-89.

[9]Platzer A.Logicalanalysisofhybridsystems:Provingtheoremsforcomplexdynamics[M]. Berlin, Germany: Springer-Verlag, 2010: 35-86.

[10]Zhai X, Chen Q, Ji S, et al. A unified modeling and verifying framework for cyber physical systems[C]//2012 12thInternationalConferenceonQualitySoftware. Xi’an,China, 2012:23-29.DOI:10.1109/qsic.2012.11.

[11]Xiong G, Zhu F, Liu X, et al, Cyber-physical-social system in intelligent transportation[J].IEEE/CAAJournalofAutomaticaSinica, 2015, 2(3): 221-228.

[12]Lü C, Zhang J, Nuzzo P, et al. Design optimization of the control system for the powertrain of an electric vehicle: A cyber-physical system approach [C]//2015IEEEInternationalConferenceonMechatronicsandAutomation. Beijing,China, 2015: 32-40. DOI:10.1109/icma.2015.7237590.

[13]Quaglia D. Cyber-physical systems: Modeling, simulation, design and validation[C]//2013 2ndMediterraneanConferenceonEmbeddedComputing. Budva,Montenegro, 2013: 102-109. DOI:10.1109/meco.2013.6601389.

[14]Kesten Y, Manna Z, Pnueli A. Verification of clocked and hybrid systems[J].ActaInformatica, 2000, 36(11): 837-912. DOI:10.1007/s002360050177.

Model and verification of safety of cyber-physical systems based on DATL

Zhou Ying Duan Pengfei Zhai Xiaoxiang Li Bixin

(School of Computer Science and Engineering, Southeast University, Nanjing 211189, China)

To solve the problem that the expression of the differential temporal dynamic logic (dTL) is weak and the temporality expression of the differential-algebraic dynamic logic (DAL) is lack, a differential-algebraic temporal dynamic logic (DATL) based on the dTL and the DAL was proposed. The differential-algebraic program (DAP) was used as the operating model and the ability of handling temporality of the dTL was introduced into the DAL. The syntax of both the DAP and the DATL formulas were defined. Both the trace semantics of DAP and the semantics of the DATL formulas were presented. The six new rules were added based on the existing rules of dTL and DAL. Finally, the safety of the aircraft collision avoidance system were modeled and verified, proving the effectiveness of the DATL.

cyber-physical systems; property verification; differential temporal dynamic logic; differential-algebraic dynamic logic; differential-algebraic temporal dynamic logic

第47卷第1期2017年1月 東南大學學報(自然科學版)JOURNALOFSOUTHEASTUNIVERSITY(NaturalScienceEdition) Vol．47No．1Jan．2017DOI：10．3969/j．issn．1001-0505．2017．01．003

2016-06-12. 作者簡介: 周穎(1974—),女,博士,講師;李必信(1969—),男, 博士,教授,博士生導師,bx.li@seu.edu.cn.

國家自然科學基金資助項目(61572008).

周穎,段鵬飛,翟小祥,等.基于DATL的信息物理融合系統(tǒng)安全性建模與驗證[J].東南大學學報(自然科學版),2017,47(1):12-17.

10.3969/j.issn.1001-0505.2017.01.003.

TP301

A

1001-0505(2017)01-0012-06