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

周 穎 段鵬飛 翟小祥 李必信

(東南大學(xué)計(jì)算機(jī)科學(xué)與工程學(xué)院, 南京 211189)

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

周 穎 段鵬飛 翟小祥 李必信

(東南大學(xué)計(jì)算機(jī)科學(xué)與工程學(xué)院, 南京 211189)

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

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

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

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

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

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

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

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

1 基本術(shù)語(yǔ)

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

1) 如果xi∈Σ為狀態(tài)變量(Σ為狀態(tài)變量、函數(shù)和謂詞關(guān)系的集合),并且θi∈Trm(Σ)(1≤i≤n)為項(xiàng),那么(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) 只有有限次地應(yīng)用約束條件1～條件4構(gòu)成的符號(hào)串才是DJ約束;

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

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

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

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

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

1) 個(gè)體常項(xiàng)符號(hào)、個(gè)體變項(xiàng)符號(hào)是項(xiàng);

2) 若φ(x1,x2,…,xn)是n元函數(shù)符號(hào),t1,t2,…,t3是n個(gè)項(xiàng),則φ(t1,t2,…,tn)是項(xiàng);

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

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

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

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

(1)

(2)

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

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

(3)

(4)

為敘述方便,將式(3)簡(jiǎn)寫(xiě)為F(ω,0,0),式(4)簡(jiǎn)寫(xiě)為G(ω,0,0).

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

2.2 DAP的跡語(yǔ)義

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

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

在混合跡定義的基礎(chǔ)上,給出了DAP的跡語(yǔ)義.

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

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

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

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

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

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 飛機(jī)避撞系統(tǒng)安全性規(guī)約

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

3 CPS屬性驗(yàn)證

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

([;])

([α])

下面利用DATL的相繼式演算來(lái)證明公式ψ.演算過(guò)程要用到的規(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中演算過(guò)程右分支的左邊部分

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中演算過(guò)程右分支的右邊部分

由此可知,圖4中演算過(guò)程的2個(gè)分支都以*結(jié)束.

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

如果在演算過(guò)程的最后不能以*結(jié)束,則說(shuō)明DATL無(wú)法驗(yàn)證該屬性,即無(wú)法得出該屬性滿足與否的結(jié)論,需改用其他方法進(jìn)行驗(yàn)證.

4 結(jié)語(yǔ)

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

DATL能夠?qū)Υ笠?guī)模的系統(tǒng)進(jìn)行屬性驗(yàn)證,除了本文中提到的飛機(jī)避撞系統(tǒng)外,還能對(duì)列車控制系統(tǒng)、智能電網(wǎng)系統(tǒng)、汽車自動(dòng)駕駛系統(tǒng)等進(jìn)行屬性驗(yàn)證. 下一步需考慮向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].自動(dòng)化學(xué)報(bào).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月 東南大學(xué)學(xué)報(bào)(自然科學(xué)版)JOURNALOFSOUTHEASTUNIVERSITY(NaturalScienceEdition) Vol．47No．1Jan．2017DOI：10．3969/j．issn．1001-0505．2017．01．003

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

國(guó)家自然科學(xué)基金資助項(xiàng)目(61572008).

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

10.3969/j.issn.1001-0505.2017.01.003.

TP301

A

1001-0505(2017)01-0012-06