彭 成，王盼卿

（軍械工程學(xué)院 河北 石家莊 050003）

自從20世紀60年代中期由于軟件規(guī)模越來越龐大，結(jié)構(gòu)也越來越復(fù)雜，環(huán)境的復(fù)雜性，應(yīng)用領(lǐng)域的復(fù)雜性，交流的復(fù)雜性，爆發(fā)了軟件危機．軟件開發(fā)費用和進度失控，軟件的可靠性差，生產(chǎn)出來的軟件難以維護，用戶對＂已完成＂的系統(tǒng)不滿意現(xiàn)象經(jīng)常發(fā)生，如何開發(fā)軟件，以滿足不斷增長、日趨復(fù)雜的需求；如何維護數(shù)量不斷膨脹的軟件產(chǎn)品等一系列問題始終困擾著軟件開發(fā)人員，為了解決軟件危機，軟件開發(fā)人員提出了兩種解決問題的方法，一種就是眾所周知的軟件工程方法，即把工程的思想引入軟件開發(fā)，另外一種方法就是形式化方法．形式化方法用于軟件開發(fā)可以保證軟件的正確性。形式化方法基于嚴格的數(shù)學(xué)，在軟件開發(fā)過程中使用數(shù)學(xué)具有如下優(yōu)點：數(shù)學(xué)是準確的建模媒體，能夠?qū)ΜF(xiàn)象、對象、動作等進行簡介、準確的描述；數(shù)學(xué)支持抽象，它使得規(guī)格的本質(zhì)可以被展示出來，并可以以一種有組織的方式來表示系統(tǒng)規(guī)格中的抽象層次；數(shù)學(xué)提供了高層確認的手段，可以使用數(shù)學(xué)證明來揭示規(guī)格中的矛盾和不完整性，以及用來展示設(shè)計和規(guī)格之間的一致性情況[1]。

1 形式化方法的發(fā)展

形式化方法（Formal Method）的基本含義是借助數(shù)學(xué)的方法來研究計算機科學(xué)中的有關(guān)問題.《Encyclopedia of Software Engineering》對形式化方法定義為:“用于開發(fā)計算機系統(tǒng)的形式化方法是基于數(shù)學(xué)的用于描述系統(tǒng)性質(zhì)的技術(shù)。這樣的形式化方法提供了一個框架，人們可以在該框架中以系統(tǒng)的方式刻劃、開發(fā)和驗證系統(tǒng)”[2]。換言之，在軟件開發(fā)的全過程中，凡是采用嚴格的數(shù)學(xué)語言，具有精確的數(shù)學(xué)語義的方法，都稱為形式化方法。

在邏輯科學(xué)中是指分析、研究思維形式結(jié)構(gòu)的方法。它把各種具有不同內(nèi)容的思維形式（主要是命題和推理）加以比較，找出其中各個部分相互聯(lián)結(jié)的方式，如命題中包含概念彼此間的聯(lián)結(jié)，推理中則是各個命題之間的聯(lián)結(jié)，抽取出它們共同的形式結(jié)構(gòu)；再引入表達形式結(jié)構(gòu)的符號語言，用符號與符號之間的聯(lián)系表達命題或推理的形式結(jié)構(gòu)。例如，把全稱肯定命題，用符號形式化為“SAP”；把聯(lián)言命題、假言命題分別形式化為:“p∧q、“p→q”。 又例如:一個具體的假言聯(lián)言推理“如果這種金屬是純鋁，那么它的物理性質(zhì)必與純鋁相同；如果這種金屬是純鋁，那么它的化學(xué)性質(zhì)必與純鋁相同；但這種金屬的物理性質(zhì)和化學(xué)性質(zhì)與純鋁不相同；所以，它不是純鋁。”這個推理的形式結(jié)構(gòu)是:“如果p，則q；如果p，則 r；非 q且非 r；所以非 p?！笨蛇M而形式化為下列公式:（（p→q）∧（p→r）∧┐q∧┐r→ ┐p。

軟件形式化方法最早是對于程序設(shè)計語言編譯技術(shù)的研究，即J.Backus提出的BNF描述Algol60語言的語法，出現(xiàn)了各種語法分析程序自動生成器以及語法制導(dǎo)的編譯方法，使得編譯系統(tǒng)的開發(fā)從＂手工制作方式＂發(fā)展成具有牢固理論基礎(chǔ)的系統(tǒng)方法.經(jīng)過30多年的研究和應(yīng)用，如今人們在形式化方法這一領(lǐng)域取得了大量重要的成果，從早期最簡單的形式化方法一階謂詞演算方法到現(xiàn)在的應(yīng)用于不同領(lǐng)域、不同階段的基于邏輯、狀態(tài)機、網(wǎng)絡(luò)、進程代數(shù)、代數(shù)等眾多形式化方法。形式化方法的發(fā)展趨勢逐漸融入軟件開發(fā)過程的各個階段，從需求分析、功能描述（規(guī)約）、（體系結(jié)構(gòu)/算法）設(shè)計、編程、測試直至維護。隨著形式化研究的熱潮，涌現(xiàn)出了多種形式化方法如：RSL（RAISE specification Language），B，VDM（Vienna Development Method），Z 等等。 因此，在具體的軟件開發(fā)中選擇何種形式化方法顯得至關(guān)重要。

圖1 常規(guī)方法和形式化方法的比較Fig.1 Comparison of the conventional method and formal method

2 與常規(guī)軟件工程方法比較

隨著信息社會的不斷發(fā)展，軟件系統(tǒng)開發(fā)呈現(xiàn)出復(fù)雜化的趨勢，伴隨著軟件系統(tǒng)越來越龐大，常規(guī)的軟件工程方法顯得力不從心，而形式化方法對于開發(fā)大規(guī)模、復(fù)雜的系統(tǒng)顯得游刃有余。

形式化方法和工程界的常規(guī)方法相比有明顯的區(qū)別.它們的開發(fā)原則不同:形式化方法希望能直接構(gòu)造出盡可能正確的系統(tǒng)；而常規(guī)方法主要是通過測試來發(fā)現(xiàn)系統(tǒng)的錯誤[3]。形式化方法和常規(guī)方法開發(fā)方法的比較如圖1所示。

為了更加直觀的展示形式化語言的特性，我們通過在企業(yè)員工管理系統(tǒng)中雇員信息管理中兩種方法的對比可以看出形式化方法基于嚴格的數(shù)學(xué)的優(yōu)勢。用自然語言描述系統(tǒng)功能為：將一個公司雇員的信息登錄到數(shù)據(jù)庫；檢查一個雇員的信息是否已經(jīng)登錄到數(shù)據(jù)庫；返回當(dāng)前在數(shù)據(jù)庫中登錄的雇員人數(shù)[4]。

形式化方法規(guī)格說明（RSL）

scheme STAFFDATABASE=

class

type

Staff，

StaffDB=Staff-Set

value

empty:StaffDB，

register:Staff×StaffDB→StaffDB，

check:Staff×StaffDB→Bool，

number:StaffDB→Nat

axiom

empty≡{}

?s:Staff，stb:StaffDB·register（s，stb）≡{s}∪stb

?s:Staff，stb:StaffDB·check （s，stb）≡s∈ stb

?stb:StaffDB·number（stb）≡card stb

end

傳統(tǒng)的常規(guī)方法對問題的描述易出現(xiàn)矛盾、二義性和含糊性，缺乏準確的語義對模型難以進行一致性檢查和正確性分析，進而限制其有效性。而對于形式化方法來說，由于其基于嚴格的數(shù)學(xué)，具有嚴格的語法和語義定義，從而可以準確的描述系統(tǒng)模型，排除了矛盾、二義性、含糊性等情況。

3 形式化方法選擇策略

3.1 常用的軟件形式化方法

常用的軟件形式化方法有RSL，B，VDM，Z等等。

1）RSL

RSL代表RAISE規(guī)格說明語言。RAISE是Rigorous Approach to Industrial Software Engineering的縮寫，指面向工業(yè)軟件工程的嚴格方法[5]。RAISE是在一個廣譜的規(guī)范語言基礎(chǔ)上，提供一系列工具和轉(zhuǎn)換技術(shù)，形成一種開發(fā)軟件的嚴格方法。它既可以用于書寫非常抽象的、初級的規(guī)范，也可以用于書寫易于自動轉(zhuǎn)換到程序語言的更具體的規(guī)范。

2）B

B是目前國際上最受重視的實用性軟件形式化方法之一，B語言是由Z語言發(fā)展而來的，其目的是為這種形式化方法增強模塊能力和工具支持能力。B語言稱為一種廣譜語言和方法，它既包括高度抽象的數(shù)學(xué)描述，又包括了可執(zhí)行的描述。B語言支持規(guī)格說明，并且支持繼規(guī)格說明之后所有的精化和設(shè)計步驟[6]。

3）Z

Z規(guī)格說明語言是在1979年由J.Abrial和S.Schumann最早提出的，而后由Hoare所領(lǐng)導(dǎo)的牛津大學(xué)程序設(shè)計研究小組（PRG）進行了大量的研究工作[7]。Z語言以一階謂詞邏輯和集合論作為形式語義基礎(chǔ)，利用集合、序列、包等數(shù)學(xué)概念對目標軟件的結(jié)構(gòu)特性和行為特性進行抽象描述，它具有簡明、精確、無歧義的優(yōu)點[8]。成功的應(yīng)用例子有英國Hursley的IBM公司將 Z應(yīng)用到 CICS（Custom lnformation and Control System）系統(tǒng)軟件，牛津大學(xué)的PRG將Z應(yīng)用于為Transputer Inmos T800版本提供的浮點運算支持等。

4）VDM

VDM是由IBM公司維也納實驗室的研究小組于20世紀70年代提出來的一種形式化方法。VDM建立的初衷，是為了實現(xiàn)PL/1語言的嚴密、精確語義規(guī)格。20世紀70年代末至80年代初，VDM在歐洲開始得到推廣應(yīng)用，它先是應(yīng)用于開發(fā)程序語言的語義形式說明，以后逐漸成為一般軟件的開發(fā)方法。進入20世紀90年代，VDM在歐美許多研究機構(gòu)和大學(xué)得到了廣泛的應(yīng)用，當(dāng)時一些大學(xué)，如英國的曼徹斯特大徐等，將VDM作為大學(xué)計算機系的必修課程。1996年，國際標準化組織ISO制訂了VDM的國際化標準版本VDM-SL.目前，VDM已成為應(yīng)用最為廣泛的形式化規(guī)格語言之一。

4.2 特點分析

所有的形式化方法都是以數(shù)學(xué)為基礎(chǔ)的.RSL和Z都是基于集合論和一階謂詞演算的，Z中還包含有模式的概念，B以集合論為基礎(chǔ)，B的語義是建立在Abrial廣義替換語言和用謂詞變換和擴展的Dijkstra最弱前置條件演算基礎(chǔ)上。VDM的基礎(chǔ)是集合論和部分函數(shù)。

形式化方法采用基于模型（Model-oriented）或基于性質(zhì)（Property-oriented）的方法，并且方法的嚴格化程度不同。基于模型的形式化利用一些已知特性的數(shù)學(xué)抽象來為目標軟件系統(tǒng)的狀態(tài)特征和行為特征構(gòu)造模型?；谔匦缘男问交椒ú恢苯佣x系統(tǒng)的行為，而是用一組公理的形式來描述系統(tǒng)的各種性質(zhì)。

B，VDM，Z是基于模型的方法，RSL是兩種方法的混合體。

VDM是B，Z，VDM，RSL中最早的一種語言，其實VDM不僅是一種語言，還是一種開發(fā)方法，RSL與VDM是三值邏輯（真、假、未定義的），B，Z 是二值邏輯（真，假），但 VDM 沒能提供組裝/分解規(guī)格說明和精化的機制。

RSL與VDM都能描述系統(tǒng)功能，用于順序程序的設(shè)計，并可描述并發(fā)，B和Z只能描述系統(tǒng)功能和順序程序的設(shè)計。

RSL和B都具有廣譜的特性，而VDM和Z都沒有，B，VDM和Z都已經(jīng)有了國際標準，RSL到目前為止還沒有國際標。4種語言的特點比較如表1所示。

表1 4種形式語言特點的比較Tab.1 Comparison of the four forms of language features

3.3 選擇策略

基于以上分析我們可以得出如下的選擇策略：對于所要開發(fā)的系統(tǒng)具有時間跨度長、經(jīng)費充足、軟件質(zhì)量要求高而且軟件開發(fā)小組的人員素質(zhì)高，對形式化方法比較了解的情況，我們推薦采用形式化的開發(fā)方法；具體來講，當(dāng)所要開發(fā)的系統(tǒng)中帶有較多并發(fā)操作時選擇RSL，VDM形式規(guī)格說明過于形式化往往不容易理解，因而VDM適合對本方法特別熟悉的軟件開發(fā)小組，B語言是一種支持從規(guī)格說明到代碼生成整個開發(fā)過程的形式化方法，因此需要軟件自動化程度高的系統(tǒng)開發(fā)推薦使用B方法。軟件系統(tǒng)的Z模式規(guī)格說明可以按一定的層次結(jié)構(gòu)給出。模式的使用為規(guī)格說明提供了一種演算，通過這種演算無論多么大型系統(tǒng)的規(guī)格說明都可以通過一個個小的部分來構(gòu)成，因此Z適合于規(guī)模較為龐大的巨系統(tǒng)的研發(fā)。

4 結(jié)束語

本文介紹了解決軟件危機的除軟件工程外的另一種方法：形式化方法，形式化方法利用了數(shù)學(xué)的嚴密性來解決在軟件危機中出現(xiàn)的各種歧義性等問題，并給出了幾種常用的形式化方法：RSL，B，VDM，Z，然后對它們的特點進行了分析比較，并給出了適合形式化方法的情況和形式化方法選擇策略?？梢灶A(yù)計，在將來形式化方法可能會融入到信息技術(shù)的各個領(lǐng)域并成為一種主流的方法和技術(shù).

[1]李瑩，吳江琴.軟件工程形式化方法與語言[M].浙江：浙江大學(xué)出版社，2010.

[2]焦蕾.Agent結(jié)構(gòu)的形式化描述及研究 [J].電子設(shè)計工程，2012，16（4）：51-55.JIAO Lei.Description and study of Agent structure[J].Electronic Design Engineering，2012，16 （4）:51-55.

[3]Milner R.A complete inference system for a class of regular behaviors[J].Journal of Computer and System Sciences，2009，28（3）:439-466.

[4]Hoare C A R.Communicating Sequential Processes[M].New York:Prentice Hall，2010.

[5]塔維娜，何積豐.基于形式化方法的需求分析[J].計算機工程，2010，26（18）:107-113.TA Jina，He Jifeng.Requirement analysis based on formal method[J].Computer Engineering，2010，26（18）:107-113.

[6]Brookes S D，Hoare C A R，Roscoe A W.A theory of communicating processes[J].Journal of the ACM，2009，31（3）:560-599.

[7]陳怡海，繆淮扣.兩種形式語言:RSL與Z的分析比較[J].計算機應(yīng)用與軟件，2002，18（4）:56-60.CHEN Yi-hai，MIAO Huai-kou.Two kinds of language:the analysisof RSLand Zin comparison[J].Computer Applications and Software，2002，18（4）:56-60.

[8]Hennessy M，Milner R.Algebraic laws for nondeterminism and concurrency[J].Journal of the ACM，2009，32（1）:137-161.