許 明，開金宇，肖 蕾，3

(1.廈門理工學院計算機與信息工程學院，福建廈門361024;2.安陽師范學院計算機與信息工程學院，河南安陽455002;3.上海大學計算機工程與科學學院，上海200027)

形式化系統(tǒng)方法是一種對形式化系統(tǒng)中形式化語言按照計算規(guī)則運算的結(jié)果依據(jù)推理規(guī)則進行邏輯推理判斷的方法.由三大部分組成.第1部分是形式化語言，由形式化語言的字符集中的字符按照一定的語法規(guī)則組成的合法字符串，即是形式化語言，也稱合式公式，記為wff.第2部分是形式化系統(tǒng)的推理機制.形式化系統(tǒng)的推理機制由兩部分組成，1)公理，不需要依據(jù)推理規(guī)則即可判斷為合法的字符串，稱為公理，記作Axioms;2)推理規(guī)則，推理規(guī)則用于操縱Axioms和(或)其他wffs產(chǎn)生新的合法字符串wffs.第3部分是對形式化系統(tǒng)中形式化語言的語義解釋.對形式化語言的語義解釋用于對無意義的形式化語言，即合式公式，賦予有意義的領域含義.對形式化語言的語義解釋通常采用自然語言，自然語言不是一種完美的形式化語言，但由于其通用性，所以在對語義解釋沒有嚴格要求下，使用自然語言對語義進行解釋.

形式化系統(tǒng)有兩個重要的性質(zhì):1)完備性;2)一致性.

假設對于形式化系統(tǒng)F，存在一些形式化語言{f1，f2，f3，…，fn}，對這些形式化語言的解釋為{I[f1]，I[f2]，I[f3]，…，I[fn]}.

如果從語義解釋的角度出發(fā)，存在從序列I[f1]= .T.，I[f2]= .T.，…，I[fk]= .T.可以語義推出I[fn]=.T.的情況下，依據(jù)形式化系統(tǒng)的推理規(guī)則可以從序列f1，f2，…，fk語法推出 fn，稱形式化系統(tǒng)F具有完備性.對完備性的解釋為:從一些語義解釋為真的合式公式集合能夠語義推出某個合式公式語義解釋為真，從這些為真的合式公式集合也能語法推出這個合式公式為真.語義推出用符號“|=”表示.語法推出用符號“|－”表示.

形式化系統(tǒng)的一致性表現(xiàn)為:如果從為真的合式公式集合，可以語法推出為真的合式公式，從這些合式公式語義解釋為真的集合也可以語義推出這個合式公式的語義解釋為真.即對于f1，f2，…，fk|－fn，都有:[f1]=.T.，I[f2]=，T.，…，I[fk]= .T.|=I[fk]=.T.稱形式化系統(tǒng) F 具有一致性.

對于一個形式化系統(tǒng)，通常不嚴格要求其滿足完備性.在使用形式化系統(tǒng)時，通常只考慮其一致性.即語法上可以推理一個合式公式為真，則從語義上，就可以得到這個合式公式為真的語義解釋.

形式化方法就是從形式化系統(tǒng)的構(gòu)建開始的.

1 形式化系統(tǒng)的發(fā)展

1.1 形式化系統(tǒng)的原型及發(fā)展

命題邏輯推理系統(tǒng)是第一個形式化系統(tǒng)，由命題邏輯語言、推理機制和語義解釋三部分組成[1].

由于命題邏輯語言的表達能力非常有限，以命題邏輯推理系統(tǒng)為基礎，通過擴大命題邏輯語言的表達能力和增加更多的推理規(guī)則，構(gòu)建了謂詞邏輯推理系統(tǒng).在謂詞邏輯推理系統(tǒng)中，形式化語言稱為謂詞邏輯語言[1].

形式化系統(tǒng)可以用于陳述理論，構(gòu)建特定理論的形式化系統(tǒng).

1.2 構(gòu)建特定理論的形式化系統(tǒng)

理論是對某種現(xiàn)象的事實進行陳述.實際上，各種理論都包含太多的事實，以至于無法明確地一一列舉.因此，對理論的陳述常通過基本事實集和特定規(guī)律來表達.通過基本事實集和特定規(guī)律以及邏輯推理規(guī)則可以判斷其他的事實現(xiàn)象是否滿足該理論.

以謂詞邏輯推理系統(tǒng)為基礎，引入對特定理論的陳述，就可以構(gòu)建特定理論的形式化系統(tǒng)，作為支撐的謂詞邏輯推理系統(tǒng)的任何性質(zhì)都自動傳承為特定理論形式化系統(tǒng)的性質(zhì).

作為特定理論陳述的形式化系統(tǒng)，常常需要將形式化語言約束到僅與特定理論相關的術(shù)語集合中，這個集合就構(gòu)成了特定理論形式化語言的字符集.

特定理論的基本事實集和特定規(guī)律構(gòu)成了特定理論形式化系統(tǒng)推理機制中的公理部分和推理規(guī)則，通過作為公理的基本事實集和作為推理規(guī)則的特定規(guī)律及謂詞邏輯推理規(guī)則，就可以判斷出其他事實現(xiàn)象是否滿足該理論.

通常，還需要對特定理論的形式化語言進行語義解釋，從而還原到研究者感興趣的這些現(xiàn)象的某個應用領域.

這樣，就構(gòu)建了一個合適的特定理論的形式化系統(tǒng).

1.3 更豐富的形式化系統(tǒng)

集合理論、關系理論、函數(shù)理論和序列理論等作為通用的數(shù)學理論都可以在謂詞邏輯推理系統(tǒng)的基礎上，通過擴大數(shù)學理論形式化語言的字符集，增加構(gòu)成數(shù)學理論形式化語言的語法規(guī)則，和增加相應的公理集和推理規(guī)則，構(gòu)建更豐富更強大的數(shù)學理論推理形式化系統(tǒng).

隨著形式化系統(tǒng)語言描述能力和邏輯推理能力的增強，可以將其應用到軟件工程領域.以通用數(shù)理系統(tǒng)為基礎，構(gòu)建軟件系統(tǒng)特定理論的形式化系統(tǒng)，將形式化系統(tǒng)理論應用于描述軟件系統(tǒng)的某些方面的特定理論.

2 構(gòu)建軟件系統(tǒng)的形式化系統(tǒng)

在一階數(shù)理邏輯語言推理系統(tǒng)的基礎上，對軟件系統(tǒng)的特定理論構(gòu)建其形式化系統(tǒng)[2－6].

2.1 軟件系統(tǒng)的分類

根據(jù)計算機軟件系統(tǒng)的系統(tǒng)行為狀態(tài)變化是否受外力作用，可以把計算機軟件系統(tǒng)分為2類:第一類是系統(tǒng)在運行過程中不受外力作用.這類系統(tǒng)的特點是以系統(tǒng)輸入為系統(tǒng)初始行為狀態(tài)，通過完成一個不受外力作用的計算過程，以產(chǎn)生系統(tǒng)輸出為系統(tǒng)終止行為狀態(tài).這類系統(tǒng)稱為變換型系統(tǒng)，記作transformation system.

第二類是系統(tǒng)在運行過程中需要不斷地維護系統(tǒng)與外界的交互，從而導致系統(tǒng)行為狀態(tài)不斷發(fā)生變化的軟件系統(tǒng).這類系統(tǒng)稱為反應型系統(tǒng)，記作reactive system.由于這類系統(tǒng)更強調(diào)系統(tǒng)行為狀態(tài)受外界環(huán)境的刺激而導致系統(tǒng)從一個行為狀態(tài)遷移到另外一個行為狀態(tài)，而不強調(diào)以產(chǎn)生系統(tǒng)輸出為目的，因此，這類系統(tǒng)也稱為遷移系統(tǒng)，記作transition system.這類計算機軟件系統(tǒng)常與硬件相結(jié)合，用于對硬件的控制，即嵌入式軟件系統(tǒng)，被廣泛應用于人類社會的各個領域.因此，從形式化方法去保證這類軟件系統(tǒng)的可靠性必將大大增強設計人員對系統(tǒng)設計和實現(xiàn)的信心.

對于變換型系統(tǒng)，系統(tǒng)行為狀態(tài)只從作為系統(tǒng)輸入的初始狀態(tài)變換到作為系統(tǒng)輸出的終止狀態(tài)，可以看作是遷移系統(tǒng)的特例，因此，作為更一般的計算機軟件系統(tǒng)模型，本文將重點介紹遷移系統(tǒng)模型.

2.2 基本遷移系統(tǒng)

以一階數(shù)理邏輯推理系統(tǒng)為基礎，構(gòu)建描述反應式軟件系統(tǒng)行為狀態(tài)變化理論的形式化系統(tǒng)，稱為基本遷移系統(tǒng).基本遷移系統(tǒng)構(gòu)建如下.

2.2.1 基本遷移系統(tǒng)的形式化語言

1)構(gòu)成形式化語言的字符集

系統(tǒng)行為狀態(tài)由構(gòu)成系統(tǒng)行為狀態(tài)的原子狀態(tài)變量按照一階數(shù)理邏輯語言的語法規(guī)則組合而成，系統(tǒng)原子狀態(tài)變量構(gòu)成了基本遷移系統(tǒng)的形式化語言的字符集，記作vocabulary，簡記為V.

V={vi|vi是原子狀態(tài)變量，i∈0∪N}}.

通常情況下假定系統(tǒng)原子狀態(tài)變量個數(shù)可數(shù);vi可以是數(shù)據(jù)狀態(tài)變量，也可以是控制狀態(tài)變量;數(shù)據(jù)狀態(tài)變量根據(jù)其取值范圍定義其數(shù)據(jù)類型，可以是布爾類型，整型，列表類型或其他類型;控制狀態(tài)變量用于表示系統(tǒng)運行過程中進程的位置，因此，控制狀態(tài)變量的取值范圍為系統(tǒng)進程的位置點集合.

此外，出于對狀態(tài)變量值發(fā)生變化進行對比的考慮，我們也把狀態(tài)變量分為不變狀態(tài)變量和可變狀態(tài)變量，不變狀態(tài)變量的值，在整個系統(tǒng)運行期間的每個狀態(tài)中都保持不變，而可變狀態(tài)變量的值，在系統(tǒng)運行期間的每個狀態(tài)中根據(jù)實際運行情況而變化.數(shù)據(jù)狀態(tài)變量和控制狀態(tài)變量都可以是可變狀態(tài)變量或不變狀態(tài)變量.

特別需要注意的是，由于在反應式軟件中，強調(diào)系統(tǒng)行為從前一個狀態(tài)遷移到下一個狀態(tài)，因此，我們假定構(gòu)成系統(tǒng)行為狀態(tài)的原子狀態(tài)變量在不同系統(tǒng)行為狀態(tài)下的取值對應的狀態(tài)變量名為}也存在于 V 中.

2)基本遷移系統(tǒng)形式化語言的語法規(guī)則

基本遷移系統(tǒng)用于描述反應式軟件系統(tǒng)行為狀態(tài)的遷移過程，系統(tǒng)行為狀態(tài)及遷移是基本遷移系統(tǒng)的形式化語言.

系統(tǒng)行為狀態(tài)的集合稱為系統(tǒng)行為狀態(tài)域，記作:

Σ ={si|si為系統(tǒng)行為狀態(tài)，i∈{0∪N}}也稱為系統(tǒng)行為狀態(tài)空間，或簡稱為系統(tǒng)狀態(tài)空間或狀態(tài)空間，通常系統(tǒng)行為狀態(tài)的個數(shù)有限.

系統(tǒng)行為狀態(tài)由來自基本遷移系統(tǒng)的形式化語言字符集V中的字符，即原子狀態(tài)變量，按照一階數(shù)理邏輯語言的語法規(guī)則構(gòu)成.

假設系統(tǒng)行為狀態(tài)sk由原子狀態(tài)變量按照一定的數(shù)理邏輯語言組成語法規(guī)則構(gòu)成，用向量 表示 ，則系統(tǒng)行為狀態(tài)sk可簡記為

使系統(tǒng)初始行為狀態(tài)s0成立的向量u0的組合項，稱為系統(tǒng)行為狀態(tài)的初始條件，記作Θ.當Θ為真時，對應的語義解釋即為系統(tǒng)初始狀態(tài)s0.

在外力作用下，系統(tǒng)從一個行為狀態(tài)遷移到下一個行為狀態(tài)，也可能從同一個行為狀態(tài)遷移到多個不同的行為狀態(tài)，這個過程用系統(tǒng)行為狀態(tài)遷移函數(shù)τ表示，簡稱為遷移函數(shù)τ，遷移函數(shù)τ是一個從Σ到的映射關系，記作τ:Σ→2Σ.

系統(tǒng)中所有遷移函數(shù)的集合用T表示，T={τ|τΣ →2Σ}，簡稱為遷移集 T.

至此，反應式軟件的系統(tǒng)行為狀態(tài)可遷移情況可以用四元組表示L={V，Σ，Θ，T}來表示.

其中:V表示組成系統(tǒng)行為狀態(tài)變量的原子狀態(tài)變量集合;Θ表示使系統(tǒng)初始行為狀態(tài)為真的原子狀態(tài)變量組成的條件表達式;Σ表示系統(tǒng)行為狀態(tài)集合;T表示系統(tǒng)行為狀態(tài)遷移函數(shù)集合.

2.2.2 基本遷移系統(tǒng)形式化語言的語義解釋

對形式化語言的語義解釋通常采用自然語言.但自然語言受其二義性局限，致使其不是一種完美的語義解釋語言，不能在計算機上進行惟一確定性計算，為了更好地使用計算機解釋基本遷移系統(tǒng)的某些特性，時序邏輯描述語言成為一種新的選擇.具體可參看時序邏輯描述語言的文獻資料，本文不再詳述.

2.2.3 基本遷移系統(tǒng)的推理機制

基本遷移系統(tǒng)的推理機制，用于推理在外力作用下，系統(tǒng)是否可以從一個行為狀態(tài)遷移到指定的行為狀態(tài).即，給定源系統(tǒng)行為狀態(tài)和外力序列，是否可以語法推出指定的系統(tǒng)行為狀態(tài).

1)基本遷移系統(tǒng)的計算模型

綜上可知，系統(tǒng)行為狀態(tài)可以通過系統(tǒng)原子狀態(tài)變量依據(jù)一定的數(shù)理邏輯語言組成規(guī)則構(gòu)成，對外力的描述也可以通過構(gòu)成外力的原子變量依據(jù)一定的數(shù)理邏輯語言組成規(guī)則構(gòu)成.對于系統(tǒng)行為狀態(tài)從sk到sk+1的遷移所受的外力，可以用ρτ(sk，sk+1)來表示，解釋為從sk到sk+1的遷移τ所受的外力用ρ來描述或者用ρτ表示.

則:在外力作用下，完成系統(tǒng)行為狀態(tài)從sk到sk+1的遷移，sk，sk+1∈∑，sk用向量表示，sk+1用向量表示，應滿足的條件是:

當條件滿足時，系統(tǒng)完成從行為狀態(tài)sk到sk+1的遷移動作，記作Action 1.記完成系統(tǒng)行為狀態(tài)遷移的動作的集合為Action.在Action 1∈Action的作用下，系統(tǒng)行為狀態(tài)從sk到sk+1的遷移，記作:sk→sk+1.

記系統(tǒng)行為狀態(tài)及遷移動作的集合為三元組→，→?∑×Action×Σ，則

(sk，Action 1，sk+1)∈→?sk→Action 1→sk+1

由此，反應式系統(tǒng)的系統(tǒng)行為狀態(tài)遷移的計算模型可由三元組T=(V，Σ，→)來表示.

2)基本遷移系統(tǒng)的計算描述

對于反應式系統(tǒng)，其作用是維護系統(tǒng)與外界不斷發(fā)生的交互，從系統(tǒng)觀察者的角度來看，表現(xiàn)為系統(tǒng)行為狀態(tài)在外力作用下的狀態(tài)遷移的序列.

設K是任意一個集合，記:

K*表示K中元素的有限序列集合;

表示K中元素的無限序列集合;

K∞表示 K*∪Kω;

序列的連結(jié)只需將兩個序列并列放在一起即可.

λ代表空序列;

|π|代表序列π的長度.

對于反應式軟件L={V，Σ，Θ，T}的計算模型T=(V，Σ ，→)而言，當集合 K= →時，→*，→－ω，→∞，λ，|π|分別代表系統(tǒng)行為狀態(tài)遷移的有限序列集合，系統(tǒng)行為狀態(tài)遷移的無限序列集合，系統(tǒng)行為狀態(tài)遷移的有限與無限序列集合，空的系統(tǒng)行為狀態(tài)遷移序列，以及系統(tǒng)行為狀態(tài)遷移序列π的長度.

定義:從s0出發(fā)的一條系統(tǒng)行為狀態(tài)遷移路徑，可以用→中的元素的序列表示，記為:ρ=(s0，α1，s1)(s1，α2，s2)…∈→∞.

定義:全路徑.如果遷移路徑p∈→*，則這條路徑是一條全路徑，記為a full path.

定義:一次計算.從系統(tǒng)行為狀態(tài)s，(s∈∑)出發(fā)的一次計算，用run=(s，p)表示，p是從 s出發(fā)的一條路徑.記 first(run)=s，path(run)=p如果p是有限序列，則last(run)為路徑p的最后一個狀態(tài).

定義:最長計算.對于 run=(s，p)，如果 p∈→*，則稱為是從s出發(fā)的最長計算，記為a maximal run.

定義:對于兩次計算 run1=(s，p1)，run2=(s，p2)如果run1≤run2，則 run稱計算 run1恰是計算run2的后綴;如果 run1＜run2，則稱計算run1是計算run2的一個后綴.

定義:兩次計算的連結(jié)，只需將兩次計算并列放在一起即可.運行的連結(jié)是一個偏序關系.run1run2:run1∈→*∧last(run1)=first(run2)，符號“=”讀作定義為.

則對于反應式軟件L={V，Σ，Θ，T}的計算模型T=(V，Σ，→)而言，從指定源系統(tǒng)行為狀態(tài)s0出發(fā)在外力作用下，是否可以語法推出指定的系統(tǒng)行為狀態(tài)sm即:是否存在這樣一條路徑p=(s0，α1，s1)(s1，α2，s2)…(si，αm，sm)∈→∞，則 last(run(s0，p))=sm.

3)基本遷移系統(tǒng)的推理

由上可知:對于反應式軟件L={V，Σ，Θ，T}的計算模型T=(V，Σ，→)而言，從指定源系統(tǒng)行為狀態(tài)s0出發(fā)在外力作用下，是否可以語法推出指定的系統(tǒng)行為狀態(tài)sm即:是否存在這樣一條路徑

p=(s0，α1，s1)(s1，α2，σ2)…(si，αm，sm)∈→∞，則 last(run(s0，p))=sm.

證明:當Θ=.T.時，s0為真.

假設α1=.T.則存在 p=(s0，α1，s1)∈→∞ 使得 last(run(s0，p))=s1

依次遞推，假設當 sm－1=.T.時，

假設αm=.T.則存在 p=(sm－1，αm，sm)∈→∞使得 last(run(sm－1，p))=sm

所以，判斷從指定源系統(tǒng)行為狀態(tài)s0出發(fā)在外力作用下，是否可以語法推出指定的系統(tǒng)行為狀態(tài)sm，轉(zhuǎn)化為判斷布爾表達式

則該問題轉(zhuǎn)換為布爾表達式的可滿足性SAT問題.由cook定理可知，布爾表達式的可滿足性SAT 問題是 NPC 問題[9].

4)NPC問題的解決方法

對于NPC類問題，由于其是非確定性計算模型下的易驗證問題，因此，解決此類問題的技術(shù)圍繞驗證展開，具體可分為兩類:ⅰ)公式推理驗證方法.依據(jù)一階邏輯語言演算系統(tǒng)的推理規(guī)則及反應式系統(tǒng)模型的推理規(guī)則，逐步推出系統(tǒng)行為狀態(tài)序列是否成立的結(jié)果.ⅱ)采用算法驗證方法，即，常規(guī)所說的模型檢驗(model checking).對于第一類方法，因為在推理過程中，需要專業(yè)的參考規(guī)則使用技能，因此，這個過程常常需要具有推理規(guī)則知識的專家介入，因此，很難將這個方法的使用過程自動化執(zhí)行.而第二類方法，采用非確定性多項式算法求解的方法，屬于暴力遍歷驗證的方式，雖然方法很粗暴，但卻因整個過程可以自動化而受到青睞.

狀態(tài)爆炸一直是制約這種方法使用的瓶頸，如何解決模型檢驗方法中的狀態(tài)爆炸問題一直是模型檢驗方法的核心問題.

3 擴展遷移系統(tǒng)模型

對于遷移型軟件系統(tǒng)，有時還需要對其他方面進行描述，現(xiàn)有的基本遷移系統(tǒng)模型就不完備了，為了彌補這個不完備的鴻溝，需要根據(jù)其他需要描述的方面對基本遷移系統(tǒng)模型在描述語言和推理規(guī)則上進行補充，以增加系統(tǒng)描述的完備性.

對于遷移軟件系統(tǒng)，有時需要刻畫其并發(fā)特性、實時特性或者混成特性，根據(jù)這些特性，分別對基本遷移系統(tǒng)模型進行擴充，得到并發(fā)系統(tǒng)[2－5]、實時系統(tǒng)[6－10]和混成系統(tǒng)的系統(tǒng)模型.復雜網(wǎng)絡系統(tǒng)是一種新型的系統(tǒng)，用計算機來模擬這類系統(tǒng)的運行規(guī)律是對當前計算機軟件形式化系統(tǒng)提出的一個新挑戰(zhàn).

4 結(jié)語

本文從形式化系統(tǒng)理論出發(fā)，介紹了形式化系統(tǒng)的組成和性質(zhì)，介紹了形式化系統(tǒng)的發(fā)展，介紹了形式化系統(tǒng)理論在描述反應式軟件系統(tǒng)行為狀態(tài)變化理論方面的應用，展示了構(gòu)建反應式軟件系統(tǒng)行為狀態(tài)變化的形式化系統(tǒng)的過程.本文為形式化系統(tǒng)方法在軟件系統(tǒng)特定理論描述方面的應用理清了脈絡，為描述更廣泛的軟件系統(tǒng)特定理論及復雜網(wǎng)絡系統(tǒng)的描述理清了思路.

[1]JIM W，MARTIN L.Software Engineering Mathematics[M].London:Addison － Wesley Pub(Sd)，1988:271.

[2]AMIR P.Applications of temporal logic to the specification and verification of reactive systems:a survey of current trends[M].New York:Springer－ Verlag New York，1986:510 －584.

[3]AMIR P，ZOHAR M.The Temporal Logic of Reactive and Concurrent Systems:Specification[M].New York:Springer－Verlag New York，1992.

[4]ZOHAR M，AMIR P.Temporal verification of reactive systems.safety.[M].London:Springer－Verlag New York，1995.

[5]NICOLA R D，VAANDRAGER F.Action versus state based logics for transition system [J].Lecture Notes in Computer Science，1990，469:407 －419.

[6]HENZINGER T A，MANNA Z，PNUELI A.Timed Transition Systems[J].Lecture Notes in Computer Science，1992，600:226－251.

[7]MANNA Z，PNUELI A.Models for Reactivity[J].Acta Informatica，1993，30(7):609 －678.

[8]張廣泉，沈一棟.混合系統(tǒng)的形式化模型[J].重慶大學學報:自然科學版，1999，22(6):53－57.

[9]王曉東.算法設計與分析[M].北京:清華大學出版社，2008.

[10]劉 陽.基于概率模型檢驗的服務流程建模與驗證[D].上海:上海大學，2012.