常玉婷, 潘海玉

(桂林電子科技大學 計算機與信息安全學院,廣西 桂林 541004)

形式規(guī)約作為形式化方法的主要內容,包括性質規(guī)約和模型規(guī)約[1]。在性質規(guī)約中,包含安全性和活性的線性時間屬性的規(guī)約對于系統(tǒng)驗證有著非常重要的作用。直觀上說,安全性是指“壞”的事情永遠不會發(fā)生,活性是指“好”的事情最終會發(fā)生[2]。例如,在系統(tǒng)運行時可能會存在多個進程,這些進程不會同時進入臨界區(qū),這就保證了系統(tǒng)的安全性;若某個進程在等待區(qū),則它最終會進入臨界區(qū),這就保證了系統(tǒng)的活性。

在過去的幾十年中,線性時間屬性已經得到了廣泛研究。Lamport[3]首先引入安全性和活性的概念。隨后Alpern等[4]在此基礎之上證明了任何一個線性時間屬性都可表達為安全性和活性的交集。進一步,Alpern等[5]又從自動機角度對安全性和活性進行研究,首次給出安全性和活性的Büchi自動機刻畫。Sistla[6]的研究表明,安全性和活性可通過線性時態(tài)邏輯公式進行邏輯刻畫。Kupferman等[7]提出了一種檢測LTL公式是否是安全性公式的算法,通過給定的安全性構造一個檢測壞前綴的Büchi自動機,同時構造了一個緊密自動機對已收集的中間數(shù)據進行分析,以防雙指數(shù)爆炸。除此之外,還有許多有關線性時間屬性的研究[8]。

近年來,人們開始研究在概率、模糊和度量等背景下系統(tǒng)的量化驗證問題。Kupferman等[9]通過加入概率組件,引入了一種概率壞前綴的概念,以此擴展安全性在實際驗證中的適用性。Faran等[10]利用概率給出安全等級的定義,并研究了利用確定性和非確定性自動機及線性時態(tài)邏輯公式來確定語言的安全等級的問題。李永明等[11]將經典遷移系統(tǒng)與模糊理論中的不確定性相結合,定義了可能性遷移系統(tǒng)的概念,并提出一種可能性測度方法,在此基礎上定義模糊線性時間屬性。此外,李永明等[12]將線性時間屬性推廣到多值邏輯上,根據Heyting代數(shù)理論,定義了真值度的概念,并給出安全性和活性在多值邏輯中的定義。Alfaro等[13]提出了度量遷移系統(tǒng)的概念,利用度量空間理論[17]來刻畫線性時間屬性,并給出了線性時態(tài)邏輯在度量空間上的一種擴展形式。除了研究線性時間屬性,人們還研究了分支時間屬性[18]及模型檢測[14-16]等在概率、模糊和度量等背景下的性質。

文獻[11]根據格的理論給出真值度的概念,并提出安全性和活性,但基于真值度的計算方式不能很好地刻畫系統(tǒng)和屬性之間的滿足程度。鑒于此,采用度量理論中的線性距離來量化系統(tǒng)多大程度滿足線性時間屬性,這個距離的值是系統(tǒng)與屬性之間距離差值的絕對值,若距離小于一個值,且值的范圍為[0,1],則表示系統(tǒng)滿足屬性的近似程度,值越小表示近似程度越高,當值為0時,表示系統(tǒng)滿足這個屬性。將線性距離與模糊理論相結合,采用距離刻畫系統(tǒng)與屬性之間關系的方法,定義出近似安全性與近似活性來量化系統(tǒng)滿足其屬性的程度。

1 近似線性時間屬性

1.1 線性距離

命題距離DP、跡距離DT及線性距離D分別刻畫了賦值之間的關系、(V(AP))ω中串之間的關系及FLT屬性之間的關系[12],定義分別如下:(V(AP))ω,下列結論成立:

1)Df(σ^,pref(P1))≤α,當且僅當存在σ∈(V(AP))ω,使得D(σ^σ,P1)≤α;

2) 若D(P1,P2)≤α,則Df(pref(P1),pref(P2))≤α。

證明 1)從左推右:設Df(σ^,pref(P1))≤α,則存在ρ^∈pref(P1),有DfT(σ^,ρ^)≤α。 令σ∈(V(AP))ω,且ρ^σ∈P1。將σ^擴展為σ^σ。根據跡距離的定義,

1.2 近似安全性和近似活性

在系統(tǒng)運行過程中,安全性保證“壞”的事情不會發(fā)生。經典安全性的定義[2-3]有2種不同的定義形式,分別從好前綴和壞前綴定義而來,具體如下。

1)設P為AP上的線性時間(linear-time, 簡稱LT)屬性。對于所有跡σ∈(2AP)ω,若對任意i≥0,存在σ′∈(2AP)ω,使得σ≤iσ′?P,則σ?P,稱P是一個安全性。

2)設P為AP上的LT 屬性,若對所有跡σ∈(2AP)ω,且σ?P,存在σ^∈pref(σ),使得對任意σ′∈(2AP)ω,σ^σ′?P,則稱P是一個安全性。這里稱σ^為P的一個壞前綴。

通過引入距離閾值α,將好前綴的定義從經典安全性推廣到近似安全性。具體定義如下。

定義1 設P為AP上的FLT 屬性,α∈[0,1]。對所有σ∈(V(AP))ω,若對任意i≥0,存在σ′∈(V(AP))ω,使得D(σ≤iσ′,P)≤α,則D(σ,P)≤α,稱P是一個α-安全性。

對于一個0-安全性P,由定義1 知,對任意i≥0,存在σ′∈(V(AP))ω,使得D(σ≤iσ′,P)=0,則D(σ,P)=0,即σ∈P。因此,0-安全性就是經典的安全性。

相較于安全性,活性保證“好”的事情最終會發(fā)生。經典活性的定義[3]為:設P為AP上的LT 屬性,若對任意σ^∈(2AP)*,存在σ′∈(2AP)ω,使得σ^σ′?P,則稱P是一個活性。

與近似安全性類似,以下給出活性的一種定量推廣形式——α-活性。

定義2 令α∈[0,1],P為AP上的FLT屬性。若對任意σ^∈(V(AP))*,存在σ′∈(V(AP))ω,有D(σ^σ′,P)≤α,則稱P是一個α-活性。

對于一個0-活性P,由定義2知,對任意σ^∈(V(AP))*,存在σ′∈(V(AP))ω,有D(σ^σ′,P)=0,即σ^σ′∈P。因此,0-活性就是經典的活性。

2 近似線性時間屬性的邏輯刻畫

模糊遷移系統(tǒng)是一個五元組F=(S,→,s0,AP,L),其中:S為狀態(tài)集合;→?S×S為遷移關系;s0∈S為初始狀態(tài);AP為原子命題集合;L:S→V(AP)為標記函數(shù)。

由定義知,模糊遷移系統(tǒng)和經典遷移系統(tǒng)的主要區(qū)別是標記函數(shù)。根據文獻[2],經典遷移系統(tǒng)的標記函數(shù)為L:S→2AP,狀態(tài)上的標記是原子命題集合中的元素。而本研究的模糊遷移系統(tǒng),其狀態(tài)上的標記是原子命題AP的一個賦值。

模糊遷移系統(tǒng)可表示為帶標簽的有向圖,如圖1所示。圖中的圓圈表示系統(tǒng)的狀態(tài),圓圈中的符號代表該狀態(tài)名,圓圈旁邊的部分表示該狀態(tài)上原子命題的賦值,若賦值為0,則省略該原子命題。例如,狀態(tài)s1是模糊遷移系統(tǒng)的一個狀態(tài),s1的標記函數(shù)為L(s1),則根據圖1可知,L(s1)(p)=0.7,L(s1)(r)=0.4。在狀態(tài)s2中原子命題r賦值為0,故省略。圖1中的有向邊表示狀態(tài)之間的遷移,一條無出發(fā)結點的有向邊指向的狀態(tài)為初始狀態(tài),如狀態(tài)s0是該模糊遷移系統(tǒng)的初始狀態(tài)。

圖1 模糊遷移系統(tǒng)

定義3[19]給定原子命題集AP,AP上的FLTL公式的語法遞歸定義為

其中,p∈AP,c∈[0,1]。

以下給出FLTL 公式在(V(AP))ω上的語義解釋。

給定一個FLTL公式φ和閾值α∈[0,1],φ在α約束下表示一個FLT屬性Lα(φ),定義為

若Lα(φ)是一個α-安全性,則稱φ為α-安全性公式;同樣,若Lα(φ)是一個α-活性,則稱φ為α-活性公式。因當α取值為0時,α-安全性和α-活性即為經典的安全性和活性,因此,此時α-安全性公式和α-活性公式為安全性公式和活性公式。

定理1 設p∈AP,c∈[0,1],且α∈[0,1]。在FLTL公式中,以下結論成立:

1)true和p?c-是α-安全性公式;

2)若φ1、φ2 是α-安全性公式,則φ1 ∧φ2,φ1 ∨φ2,Xφ1,Gφ1 和φ1Wφ2 也是α-安全性公式。

這里只證明p?c-。 其余證明與文獻[19]的證明類似。

設對所有σ∈(V(AP))ω,D(σ,Lα(φ))＞α,則對任意ρ∈Lα(φ),有DT(σ,ρ)＞α。 根據跡距離DT的定義,存在i∈N,使得DP(σi,ρi)＞α。 設i=0時,DP(σ0,ρ0)≤α。此時,對任意的p∈AP,|σ0(p)-ρ0(p)|≤α。 將ρ0擴展為無限跡ρ′=ρ0σ1σ2…,則

要判斷φ是否是0.2-安全性公式,只需判斷Lα(φ)是否為0.2-安全性。設σ∈L0.2(φ)且σ?P,則存在j≥0,使得σj(p)≥0.8且σj(r)≥0.8。根據定義4,

定理2 令α∈[0,1]。在FLTL公式中,以下結論成立:

1)當α∈[0,1)時,true是α-活性公式;

2)p?c-是α-活性公式;

3)若φ1 和φ2 是α-活性公式,則φ1 ∧φ2 是α-活性公式;

4)若φ1 或φ2 是α-活性公式,則φ1 ∨φ2 是α-活性公式;

5)若φ2是α-活性公式,則φ1Uφ2和φ1Wφ2都是α-活性公式;

6)若φ1是α-活性公式,則Xφ1和Fφ1都是α-活性公式。

2)令φ=p?c-。設φ不是α-活性公式,則存在^σ∈ (V(AP))*,對 任 意σ′ ∈ (V(AP))ω,有D（^σσ′,Lα(φ)）＞α。令^σσ′=σ。由線性距離D的定義知,對任意ρ∈Lα(φ),TD(σ,ρ)＞α。進一步,由跡距離DT的定義,存在i≥0,使得DP(σi,ρi)＞α。又根據定理1的證明,當i=0時,DP(σ0,ρ0)＞α,因此

因此φ是α-活性公式。

3)設φ1 和φ2 是α-活性公式。令φ=φ1 ∧φ2,σ∈Lα(φ),根據Lα(φ)的定義,‖φ‖(σ)＞α,即

所以‖φ1‖(σ)＞α且‖φ2‖(σ)＞α,即σ∈Lα(φ1)且σ∈Lα(φ2)。因為φ1和φ2是α-活性公式,則對任意^σ∈(V(AP))*,存在σ′∈(V(AP))ω,有

因此φ是α-活性公式。

4)設φ1 或φ2 是α-活性公式。令φ=φ1 ∨φ2,σ∈Lα(φ),根據Lα(φ)的定義,‖φ‖(σ)＞α,即

所以有‖φ1‖(σ)＞α或‖φ2‖(σ)＞α,即σ∈Lα(φ1)或σ∈Lα(φ2)。不妨設σ∈Lα(φ1)。當φ1是α-活性公式時,對任意^σ∈(V(AP))*,都存在σ′∈(V(AP))ω,有D(^σσ′,Lα(φ1))≤α。因此,存在ρ∈Lα(φ1),使得DT(^σσ′,ρ)≤α。故

φ1是α-活性公式,所以Fφ1 是α-活性公式。

例2 設AP={p,r},V(AP)為AP在[0,1]f上所有賦值的集合。令P是一個0.5-活性,對所有σ∈P滿足:任意i≥0,σi(p)＜0.5或σi(r)＜0.5?，F(xiàn)在使用FLTL公式描述該屬性。令

根 據L0.5(φ)的 定 義,σ∈L0.5(φ)。 故P?L0.5(φ)。綜上所述,Lα(φ)=P成立,所以(p?1)U(r?1)是0.5-活性公式。

3 實例

考慮一個由墻、窗戶、加熱器和控制器組成的房間。控制器的目的是盡可能將溫度維持在用戶舒適的范圍。因為“舒適”是一個模糊的概念,人們不能很精確地將“舒適”的意思描述出來,每個人對“舒適”的描述也會不一樣,所以可以將“舒適”一詞通過以下模糊集的定義來解釋[21-23]:

其中:Te(t)為室外溫度;T(t)為當前室內溫度;E(t)為特定于墻體和窗戶的熱交換系數(shù);H(t)為加熱器的功率。

假設溫度控制器可接收的溫度范圍為10～45℃,當室內溫度低于17℃時,加熱器開啟;當室內溫度高于24℃時,加熱器關閉;當室溫處于20～22℃時,加熱器處于睡眠模式,當處于睡眠模式的時間超過60 min時,加熱器將自動關閉。設置控制器每30 min接收一次溫度讀數(shù),然后判斷是否對加熱器進行開或關或睡眠的操作。

對房間溫度的舒適度演化進行建模。設

其中,S={s0,s1,s2},AP={t,c},其中:狀態(tài)s0表示加熱器處于關閉狀態(tài);狀態(tài)s1表示加熱器處于加熱狀態(tài);狀態(tài)s2表示加熱器處于睡眠狀態(tài);c表示當前溫度下用戶的舒適度;t表示溫度系數(shù)(即當前溫度/100),AP的賦值是在[0,1]范圍內。為了方便計算,所有的數(shù)值均保留小數(shù)點后3位。設加熱器開啟的功率為0.06℃/min,睡眠模式的功率為0.03℃/min。墻體和窗戶的熱交換系數(shù)為0.005℃/min。令i≥1,可使用公式[22]

計算大約30imin后的室溫,再通過x求μc。 公式所計算的具體值如表1所示。

根據表1,可以構建FTS。如圖2所示,此時室溫為16℃,加熱器處于關閉狀態(tài)。由于溫度低于17℃,開啟加熱器,到達狀態(tài)s1。在30 min后,溫度控制器接收當前室溫,根據上述公式,計算可得室溫為17.65℃,此時用戶舒適度仍為0,繼續(xù)處于狀態(tài)s1。通過計算,在i=4,即120 min后,室內溫度將升至約20.3℃,此時用戶舒適度約為0.767,此時加熱器切換為睡眠模式,到達狀態(tài)s2。 由于加熱器處于睡眠模式的時間超過60 min,加熱器i=7時切換為關閉狀態(tài)s1。這里不再考慮在加熱器從睡眠模式關閉后的情況。

圖2 FTS

表1 溫度控制器接收t及s和c的關系

所構建的FTS有2個屬性需要考慮:一是“安全性”,就是用戶一直感到舒適;二是“活性”,就是最終會到達一個合適的舒適度范圍。假設滿足安全性的“好”的舒適度范圍為[0.6,0.9],而滿足活性的合適的舒適度范圍為[0.6,1]。

首先考慮安全性的規(guī)范。根據圖2,令P是一個FLT屬性,且P是一個0.1-安全性,對所有σ∈P滿足:任意i≥0,0.6≤σi(c)≤0.9。因為“安全性”是要保證一直在舒適度的范圍,所以使用FLTL公式中的G描述該系統(tǒng)所刻畫的安全性。令φ=G(c?1),根據Lα(φ)的定義,

因此,G(c?1)是0.1-安全性公式。0.1-安全性表示:該系統(tǒng)所滿足的舒適度范圍和滿足安全性的舒適度范圍之間,只要保證在0.1誤差以內,都可視為是“安全”的。

根據圖2,令P為一個FLT 屬性,且P是一個0.3-活性,對所有σ∈P滿足:存在i≥0,σi(c)＜0.7。因為“活性”是最終要處于舒適的狀態(tài),所以使用FLTL公式中的F描述該屬性。令φ=F(c?1),根據Lα(φ)的定義,所以,σ?L0.3(φ),這與假設矛盾。故σ∈P,L0.3(φ)?P。 設σ∈P,則存在i≥0,σi(c)＜0.7。根據定義4,

根據L0.3(φ)的 定 義,σ∈L0.3(φ)。 故P?L0.3(φ)。綜上所述,Lα(φ)=P成立,所以F(c?1)是0.3-活性公式。0.3-活性表示:該系統(tǒng)所滿足的舒適度范圍和滿足活性的舒適度范圍之間,只要保證在0.3誤差內,都可以視為系統(tǒng)滿足該屬性。

4 結束語

研究了模糊背景下的近似安全性和近似活性及其邏輯和自動機刻畫。通過引入距離閾值α∈[0,1],定義了α-安全性和α-活性,并通過一些例子來描述所給出的定義,最后通過模糊線性時態(tài)邏輯公式給出近似安全性和近似活性的邏輯刻畫。下一步將考慮研究模糊背景下近似安全性和近似活性相關驗證算法及自動機的刻畫。