許 明，開(kāi)金宇，肖 蕾，3

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

設(shè)K是任意一個(gè)集合，記:

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

表示K中元素的無(wú)限序列集合;

K∞表示 K*∪Kω;

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

λ代表空序列;

|π|代表序列π的長(zhǎng)度.

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

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

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

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

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

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

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

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

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

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

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

證明:當(dāng)Θ=.T.時(shí)，s0為真.

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

依次遞推，假設(shè)當(dāng) sm－1=.T.時(shí)，

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

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

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

4)NPC問(wèn)題的解決方法

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

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

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

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

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

4 結(jié)語(yǔ)

本文從形式化系統(tǒng)理論出發(fā)，介紹了形式化系統(tǒng)的組成和性質(zhì)，介紹了形式化系統(tǒng)的發(fā)展，介紹了形式化系統(tǒng)理論在描述反應(yīng)式軟件系統(tǒng)行為狀態(tài)變化理論方面的應(yīng)用，展示了構(gòu)建反應(yīng)式軟件系統(tǒng)行為狀態(tài)變化的形式化系統(tǒng)的過(guò)程.本文為形式化系統(tǒng)方法在軟件系統(tǒng)特定理論描述方面的應(yīng)用理清了脈絡(luò)，為描述更廣泛的軟件系統(tǒng)特定理論及復(fù)雜網(wǎng)絡(luò)系統(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].重慶大學(xué)學(xué)報(bào):自然科學(xué)版，1999，22(6):53－57.

[9]王曉東.算法設(shè)計(jì)與分析[M].北京:清華大學(xué)出版社，2008.

[10]劉 陽(yáng).基于概率模型檢驗(yàn)的服務(wù)流程建模與驗(yàn)證[D].上海:上海大學(xué)，2012.