李 晴，曹子寧,2,3，黃 濤

(1.南京航空航天大學 計算機科學與技術學院，江蘇 南京 211106;2.光電控制技術重點實驗室，河南 洛陽 471023;3.軟件新技術與產(chǎn)業(yè)化協(xié)同創(chuàng)新中心，江蘇 南京 210023)

0 引 言

混成系統(tǒng)[1](Hybrid System，HS)通常由離散組件和連續(xù)組件組成，二者互相影響、互相依賴[2]。并且隨著混成系統(tǒng)的設計越來越復雜，二者之間的交互越來越緊密。目前，它已廣泛應用在智能電網(wǎng)、自動公路系統(tǒng)和醫(yī)療機器人等各種安全關鍵領域[3]。它們對系統(tǒng)的安全性有極高的要求，然而通過模型檢測等常用的形式化方法保障其安全性是很有限的。因此，需要將模型檢測與性能評價相結合[4]，利用各自的優(yōu)點，在保證驗證系統(tǒng)效率的同時，描述更多系統(tǒng)的屬性。

文獻[5]提出PLTL用于描述“系統(tǒng)最終不會到達死鎖狀態(tài)的概率是否小于等于0.9？”等系統(tǒng)性質。文獻[6]提出了計算樹度量語言CTML，用于評價系統(tǒng)與實數(shù)計算相關的性質，如概率、平均期望等。文獻[7]在CTML、ZIA的基礎上，提出了PZIA，用于描述系統(tǒng)與數(shù)據(jù)相關的性質和行為的概率性質等。

基于μ演算[8-9]的模型檢測可用于設計與驗證并發(fā)系統(tǒng)[10]，通過使用不動點算子刻畫系統(tǒng)的性質。文獻[11-12]在不動點算子的基礎上分別提出并發(fā)加權μ演算和廣義可能性μ演算以增強經(jīng)典μ演算的表達能力。此外，目前已有一些較為高效的算法用于評價μ演算的公式[10,13]，并且很多時序邏輯可以轉換為μ演算，比如CTL。

因此，結合CTML和μ演算，該文提出了基于不動點的性能評價語言MLBoF。由于MLBoF公式包含不動點，而不動點的存在不是必然的，因此給出其語義存在的合理性證明。為了簡化CTML子邏輯的計算步驟，給出與其語義等價的MLBoF公式及相應的證明過程。最后，給出MLBoF公式的性能評價算法。

1 性能評價語言MLBoF

為了提出能夠描述實值計算相關性質的性能評價語言，通過對經(jīng)典Kripke結構中的標簽函數(shù)進行擴展，將標簽函數(shù)L的值域從{0,1}擴展為[m,n]，其中m

定義1(狀態(tài)標簽函數(shù))：狀態(tài)標簽函數(shù)f表示從狀態(tài)空間S到閉區(qū)間[m,n]的一個映射，它可以表示為：f:S→[m,n]。其中，m和n的取值取決于具體實例。

狀態(tài)標簽函數(shù)也可稱為原子函數(shù)或狀態(tài)函數(shù)，帶有原子函數(shù)的Kripke結構定義如下：

定義2(KripkeAF)：KripkeAF結構是一個四元組MAF=(S,S0,AF,R)，其中，S是一個有限狀態(tài)集合；S0是一個有限初始狀態(tài)集合；AF是原子函數(shù)的有限集合；R是一個遷移關系，R?S×S，R滿足?s∈S,?s'∈S，使(s,s')∈R。

KripkeAF為提出可以描述系統(tǒng)實值計算相關性質的新的性能評價語言奠定了基礎。

1.1 MLBoF語法

MLBoF作為CTML和μ演算部分結合的產(chǎn)物，其語法定義如下所述：

定義3(MLBoF語法)：AF為原子函數(shù)集合，令fp表示由原子命題轉換而來的狀態(tài)函數(shù)，AF由一般的狀態(tài)函數(shù)f和fp組成。令VAR={φ1,φ2,φ3,…}，表示函數(shù)變量集合，其中每個φ∈VAR可被賦值為G(S)的一個元素，G(S)是所有可能的狀態(tài)函數(shù)組成的集合。MLBoF公式按如下規(guī)則構造：

(1)若fAF∈AF，則fAF是一個公式；

(2)一個函數(shù)變量φ是一個公式；

(3)若f和g是公式，則f·g,f∨g,f∧g也是公式；

(4)如果f是公式，那么MXf是公式；

(5)若φ∈VAR是一個公式且f是一個公式，又f在φ上是單調(diào)的(由于MLBoF公式的構造中去除了否定算子，即f中出現(xiàn)的所有函數(shù)變量φ，在公式f中其外面嵌套的否定算子個數(shù)為0)，則μφ·f和νφ·f都是公式。

1.2 MLBoF語義

經(jīng)典的μ演算公式表示一個狀態(tài)集合，而MLBoF的公式表示一個函數(shù)。MLBoF的語義定義如下所示：

定義4(MLBoF語義)：公式f可以解釋為一個狀態(tài)映射函數(shù)f:S→[m,n]，并將其記為[[f]]Me，其中M是變遷系統(tǒng)，e:VAR→G(S)是環(huán)境。函數(shù)[[f]]Me的遞歸定義如下所示：

(1)若h=[[fAF]]Me，則存在兩種情況：若fAF=f，則對于?s∈S，存在h(s)=f(s)；若fAF=fp，則對于?s∈S，存在：

(2)[[φ]]Me=e(φ)。

(3)若h=[[f·g]]Me，則對?s∈S，有h(s)=f(s)·g(s)；需要注意，使用·算子的前提是公式f和g滿足f:S→[0,1]和g:S→[0,1]，并且[0,1]?[m,n]。

(4)若h=[[MXf]]Me，則對?s∈S，有：

其中，Ts={t|s→t,且s≠t}，ps,t是由狀態(tài)s到狀態(tài)t的遷移概率。

(5)若h=[[f∧g]]Me，則對?s∈S，有h(s)=min{f(s),g(s)}。

(6)若h=[[f∨g]]Me，則對?s∈S，有h(s)=max{f(s),g(s)}。

(7)若h=[[μφ.f]]Me，則[[μφ.f]]Me是變換τ:G(S)→G(S)的最小不動點，其中τ(W)=[[f]]Me[φ←W]。

(8)若h=[[νφ.f]]Me，則[[νφ.f]]Me是變換τ:G(S)→G(S)的最大不動點，其中τ(W)=[[f]]Me[φ←W]。

2 MLBoF語義合理性

由于性能評價語言MLBoF的語義涉及到不動點，而不動點是否存在并不是顯然的。因此，MLBoF語義的合理性依賴于不動點的存在，進而下文對不動點的存在性進行論述。

根據(jù)Tarski不動點定理，若MLBoF公式的語義解釋環(huán)境構成完備格以及映射函數(shù)τ是單調(diào)的，那么可證得不動點是存在的。

下面給出基于MLBoF公式語義的G(S)上的二元關系定義，以及該二元關系是偏序關系的證明過程，具體如下：

定義5(二元關系?)：給定一個KripkeAF結構M=(S,S0,AF,R)，S上所有的狀態(tài)函數(shù)構成集合G(S)，G(S)上存在一個二元關系?：對于函數(shù)f1,f2∈G(S)，若對?s∈S，f1(s)≤f2(s)成立，則稱f1?f2成立。

命題1：G(S)上的二元關系集合(G(S),?)是偏序集。

證明：根據(jù)?和偏序的定義，可證得?滿足自反性、反對稱性和傳遞性。因此，命題1成立，具體的證明過程見文獻[14]。

命題2：偏序集(G(S),?)構成一個完備格。

證明：根據(jù)完備格[11]和(G(S),?)的定義，取G(S)中任一子集A(S)。考慮A(S)的最小上界分別是A(S)和G(S)A(S)中的元素兩種情況，可證得G(S)的任意子集A(S)存在最小上界和最大下界。具體的證明過程見文獻[14]。

在此基礎上，可以利用結構歸納法證明G(S)上的映射函數(shù)τ:G(S)→G(S)的單調(diào)性。而τ函數(shù)的單調(diào)性證明可轉化為MLBoF公式的單調(diào)性證明，進而可轉化為MLBoF公式中出現(xiàn)的所有算子的單調(diào)性證明。

命題3：MLBoF公式中出現(xiàn)的所有算子都是單調(diào)的。

證明：根據(jù)基礎算子·、MX、∧和∨的語義及利用其構造的MLBoF公式語義，可證得基礎算子·、MX、∧和∨的是單調(diào)的。因此，命題3成立，具體的證明過程見文獻[14]。

因此，由上述算子構造的MLBoF的任何公式也是單調(diào)的。由于不動點算子中的公式是·、∧、∨和MX算子構成的，所以出現(xiàn)在不動點算子中的每一個可能的公式也是單調(diào)的。根據(jù)結構歸納法，不動點算子構成的MLBoF公式也是單調(diào)的。而G(S)上的映射函數(shù)τ是由·、∧、∨和MX和不動點算子構成的，因此，根據(jù)結構歸納法，若構成τ函數(shù)的基礎算子是單調(diào)的，那么τ函數(shù)也是單調(diào)的。

由Tarski不動點定理，可知MLBoF存在最小和最大不動點。所以其語義是合理的。

利用結構歸納法的思想，可將μ演算中謂詞變換滿足∪連續(xù)和∩連續(xù)定義和性質[15]推廣到MLBoF上的映射函數(shù)τ(W)=[[f]]Me[φ←W]，因此τ(W)=[[f]]Me[φ←W]也是∪連續(xù)和∩連續(xù)的。而根據(jù)MLBoF的語法和語義可知，μφ.f和νφ.f的語義(即[[μφ.f]]Me和[[νφ.f]]Me分別表示映射函數(shù)τ(W)=[[f]]Me[φ←W]的最小不動點和最大不動點。

因此，根據(jù)Tarski不動點定理可知，若τ是∪連續(xù)的，則[[μφ.f]]Me=∪i(τi(MIN))；若τ是∩連續(xù)的，則[[νφ.f]]Me=∩i(τi(MAX))。假設G(S)中的所有函數(shù)映射的值都位于實數(shù)區(qū)間[m,n],那么MIN表示fmin:S→{m}，MAX表示fmax:S→{n}。

3 CTML子邏輯的MLBoF公式表示

3.1 CTML簡介

CTML是一個可用于描述系統(tǒng)的概率和期望等實值屬性的性能評價語言，它的某些子邏輯可以用MLBoF表示，該文將它們命名為SLoCTML(Sub-Logic of CTML)。它的語法和語義具體如下：

定義6(SLoCTML語法)：SLoCTML的語法定義如下：

(1)φ::=one|zero|r|φ·φ|Mδ；

(2)δ::=φU×φ|Xφ；

由于SLoCTML代表CTML的某些子邏輯，其更加具體的語法解釋和語義定義可見文獻[6]。

根據(jù)二者的語義，可知MLBoF公式可以表示SLoCTML，如MX、·、MU×，而且SLoCTML的原子狀態(tài)函數(shù)可以用MLBoF的原子狀態(tài)函數(shù)fp表示。

根據(jù)SLoCTML的語義可知，SLoCTML的MU×算子描述的系統(tǒng)屬性相對復雜，具有較大的實際意義。所以下文以MU×為例，給出與其語義等價的MLBoF公式表示以及證明過程。

3.2 與MU×公式語義等價的MLBoF公式

由于性能評價語言MLBoF的公式涉及到不動點，表達形式比較抽象，不利于理解和描述性質。根據(jù)二者公式語義，可知M(fU×g)與μφ.[g∨(f·MXφ)]語義等價，且τ(φ)=g∨(f· MXφ)。若狀態(tài)s滿足M(fU×g)，則使用上述語義等價的MLBoF公式計算；否則，對于不滿足路徑公式的狀態(tài)s，令其函數(shù)值為0。

在證明語義等價前，需要進行一些說明：

(1) 將SLoCTML的MU×公式中出現(xiàn)的原子命題f和g看作MLBoF中的原子函數(shù)，并且它們的值域為實數(shù)區(qū)間[m,n]中，其中m=0，n=1。

(2)令最大的狀態(tài)函數(shù)和最小的狀態(tài)函數(shù)分別為MAX:S→{n}和MIN:S→{m}。

下面給出二者語義等價的具體證明過程：

命題4：τ(φ)=g∨(f· MXφ)是單調(diào)的。

證明：假設f1?f2，根據(jù)函數(shù)τ(φ)=g∨ (f· MXφ)的語義，給出τ(f1)和τ(f2)各自可能的兩種語義。并在此基礎上，根據(jù)偏序關系?的定義、τ(f1)和τ(f2)每種可能語義之間的依賴關系，進而證得τ(f1)?τ(f2)成立。具體的證明過程見文獻[14]。

命題5：M(fU×g)的語義和τ(φ)=g∨(f·MXφ)的不動點的語義等價。

證明：綜合考慮M(fU×g)可能的兩種語義h(s)=g(s)和h(s)=(f· MX (MfU×g))(s)，利用公式轉換和具體的公式語義可證得命題5成立，具體的證明過程見文獻[14]。

命題6：CTML的M(fU×g)公式的語義和MLBoF的μφ.[g∨ (f·MXφ)]公式語義等價，即M (fU×g)=[[μφ.[g∨ (f·MXφ)]]]Me。

證明：在分析公式μφ.[g∨ (f· MXφ)]和M(fU×g)的語義之后，利用歸納法，依次證得∪i(τi(MIN))?M(fU×g)和M(fU×g)?∪i(τi(MIN))成立。因此，命題6成立。具體的證明過程見文獻[14]。

4 MLBoF公式的性能評價算法

該算法是對Emerson和Lei提出的用于評價μ演算公式的算法[15]的一個擴展，其不同之處在于在計算外層不動點的新的近似值時，不必使用MIN或MAX重新初始化內(nèi)層不動點的計算，只需從這個不動點下的任何已知的近似值開始迭代計算即可。此外，通過引入人為設置的誤差值α，避免算法進行無終止地計算。所以，該算法能夠在保證效率的同時，盡可能地計算出較為接近真正不動點的近似不動點。

MLBoF公式的性能評價算法輸入MLBoF公式、系統(tǒng)模型KripkeAF和誤差值α，輸出一個狀態(tài)函數(shù)h。該算法的偽代碼如下所示：

1:Function eval (h,e)

2:if (h=fp)

3: forsinS

4:if (p∈L(s))h(s)=1;

5:Elseh(s)=0;

6: returnh;

7:if (h=f)

8: forsinSh(s)=f(s);

9: returnh;

10:if (h=φ) returne(φ);

11:if (h=g1·g2)

12:g1=eval(g1,e);g2= eval(g2,e);

13: forsinSh(s)=g1(s)·g2(s);

14: returnh;

15:if(h=g1∧g2)

16:g1=eval(g1,e);g2= eval(g2,e);

17: forsinSh(s)=min{g1(s),g2(s)};

18: returnh;

19:if (h=g1∨g2)

20:g1= eval(g1,e);g2=eval(g2,e);

21: forsinSh(s)=max{g1(s),g2(s)};

22: returnh;

23:if(h= MXg)

24:g=eval(g,e);

25: forsinS

27: Elseh(s)=g(s);

28: returnh;

29:if (h=μφi.f(φi))

30: for top-level greatest fixpoint subformulasυφj.f'(φj) inf

31:F[j]=MAX;

32: while ?s∈S,F[j](s)-φold(s)>α

33:φold=F[i];

34:F[i]= eval(f,e[φi←F[i]]);

35:h=F[i]；

36: returnh;

37:if (h=νφi.f(φi))

38: for top-level least fixpoint subformulasμφj.f'(φj) inf

39:F[j]=MIN;

40: while ?s∈S,F[i](s)-φold(s)>α

41:φold=F[i];

42:F[i]=eval(g,e[φi←F[i]]);

43:h=F[i]；

44: returnh;

45:end function eval;

5 MLBoF性能評價公式實例

本節(jié)以飛機起飛控制系統(tǒng)[16]為例，使用MLBoF和CTML公式分別描述與其本身相關的系統(tǒng)性質，并使用MLBoF公式的性能評價算法計算MLBoF公式的值。

它的整個起飛過程由停止、滑行、起飛、爬升、平飛等階段組成，并且前四個階段有可能進入故障狀態(tài)。它的自動機模型如圖1所示。

圖1 飛機控制系統(tǒng)

(1)對于性質“飛機從Stop開始，最終發(fā)生異常即到達Error狀態(tài)的概率是多少”， CTML描述為：(Mone U×fError) (Stop)， MLBoF公式描述為：μφ.[fError∨ (one · MXφ)]，τ(φ)=fError∨ (one · MXφ)。需要注意的是，下面公式中的S的元素依次為狀態(tài)Stop、Taxi、Take_off、Climb、Error和Cruise。

其中，MLBoF公式分別由CTML中的原子命題one和fError轉換而來。因此，其映射的實數(shù)區(qū)間為[0,1]，并且MIN:S→{0}。根據(jù)性能評價算法，令誤差α=0.001，有：

τ(MIN)(S)=(0,0,0,0,1,0)；

τ2(MIN)(S)=(0.1, 0.1, 0.1, 0.1, 1, 0)；

τ3(MIN)(S)=(0.19, 0.19, 0.19, 0.1, 1, 0)；

τ4(MIN)(S)=(0.271, 0.271, 0.19,0.1,1,0)；

τ5(MIN)(S)=(0.343 9,0.271,0.19,0.1,1,0)；

τ6(MIN)(S)=τ5(MIN) (S)。

此時算法終止，可知飛機從Stop開始，最終發(fā)生異常即到達Error狀態(tài)的概率是0.343 9。

(2)對于性質“飛機從Stop開始，最終成功巡航即到達Cruise狀態(tài)的概率是多少”，CTML描述為：(M oneU×fCruise)(Stop)， MLBoF公式描述為：μφ.[fCruise∨ (one · MXφ)]，τ(φ) =fCruise∨ (one · MXφ)。

根據(jù)性能評價算法，令誤差α=0.001，有：

τ(MIN)(S) = (0, 0, 0, 0, 0, 1)；

τ2(MIN)(S) = (0, 0, 0, 0.9, 0,1)；

τ3(MIN)(S) = (0, 0, 0.81, 0.9, 0, 1)；

τ4(MIN)(S) = (0, 0.729, 0.81, 0.9, 0, 1)；

τ5(MIN)(S)=(0.656 1, 0.729,0.81, 0.9,0,1)；

τ6(MIN)(S) =τ5(MIN)(S)；

此時算法終止，可知飛機從Stop開始，最終成功巡航即到達Cruise狀態(tài)的概率是0.656 1。

通過上述應用實例可知，MLBoF公式的性能評價算法的效率體現(xiàn)在以下兩個層面：

(1)由于MU×公式的計算依賴于涉及矩陣方程等復雜計算的線性系統(tǒng)求解[6]，計算復雜，且時間復雜度為O(Poly(|S|)。其中Poly(|S|)表示|S|大小的多項式時間，|S|表示系統(tǒng)模型中的狀態(tài)個數(shù)。而與MU×公式語義等價的MLBoF公式的計算依賴于計算不動點的思想，該過程無需進行復雜的數(shù)學計算。因此，從這個層面上講，該算法的效率體現(xiàn)在算法思想和計算步驟的簡單。

(2)由于MLBoF公式的性能評價算法的提出基于對需要進行O(nd)次迭代的計算不動點的算法的擴展，相對于擴展需要進行O(nk)次迭代的簡單直接的遞歸算法，該算法的效率更高。其中，n表示系統(tǒng)模型的狀態(tài)個數(shù)，k表示不動點嵌套深度，d表示公式的交替深度[15]。因此，從這個層面上，該算法的效率也得到了一定的改善。

6 結束語

由于混成系統(tǒng)廣泛應用于各種安全關鍵領域，通過一般的形式化方法保障其安全性有一定的局限性。因此，提出一種面向混成系統(tǒng)的性能評價語言MLBoF，用于描述系統(tǒng)行為的概率屬性等。同時，為了簡化SLoCTML的計算步驟以及提高MLBoF公式的理解性，給出與SLoCTML語義等價的MLBoF公式。最后，通過擴展計算不動點的算法，提出一個MLBoF公式的性能評價算法。與傳統(tǒng)的基于μ演算的模型檢測[15]相比，MLBoF可以描述系統(tǒng)行為的概率屬性。在以后的工作中，可以嘗試往MLBoF公式中引入更多的算子如+算子，使其能夠描述完整的CTML邏輯。