軟件形式化開發(fā)方法的選擇策略研究

彭 成，王盼卿

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

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

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

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

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

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

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

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

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

形式化方法規(guī)格說(shuō)明（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ī)方法對(duì)問題的描述易出現(xiàn)矛盾、二義性和含糊性，缺乏準(zhǔn)確的語(yǔ)義對(duì)模型難以進(jìn)行一致性檢查和正確性分析，進(jìn)而限制其有效性。而對(duì)于形式化方法來(lái)說(shuō)，由于其基于嚴(yán)格的數(shù)學(xué)，具有嚴(yán)格的語(yǔ)法和語(yǔ)義定義，從而可以準(zhǔn)確的描述系統(tǒng)模型，排除了矛盾、二義性、含糊性等情況。

3 形式化方法選擇策略

3.1 常用的軟件形式化方法

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

1）RSL

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

2）B

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

3）Z

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

4）VDM

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

4.2 特點(diǎn)分析

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

形式化方法采用基于模型（Model-oriented）或基于性質(zhì)（Property-oriented）的方法，并且方法的嚴(yán)格化程度不同。基于模型的形式化利用一些已知特性的數(shù)學(xué)抽象來(lái)為目標(biāo)軟件系統(tǒng)的狀態(tài)特征和行為特征構(gòu)造模型。基于特性的形式化方法不直接定義系統(tǒng)的行為，而是用一組公理的形式來(lái)描述系統(tǒng)的各種性質(zhì)。

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

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

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

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

表1 4種形式語(yǔ)言特點(diǎn)的比較Tab.1 Comparison of the four forms of language features

3.3 選擇策略

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

4 結(jié)束語(yǔ)

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

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

[2]焦蕾.Agent結(jié)構(gòu)的形式化描述及研究 [J].電子設(shè)計(jì)工程，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].計(jì)算機(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]陳怡海，繆淮扣.兩種形式語(yǔ)言:RSL與Z的分析比較[J].計(jì)算機(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.