摘 要：軟件工程中的形式化方法是以數(shù)學(xué)理論為基礎(chǔ)，建立的一種用來(lái)解決軟件工程領(lǐng)域問(wèn)題的系統(tǒng)性分析方法。形式化方法通過(guò)具有明確語(yǔ)義的形式語(yǔ)言來(lái)描述目標(biāo)軟件系統(tǒng)的行為和特征，為目標(biāo)系統(tǒng)開(kāi)發(fā)提供了一個(gè)模型化的有效設(shè)計(jì)和分析途徑，保障了系統(tǒng)的安全性和可靠性。本文簡(jiǎn)單介紹了形式化方法的研究?jī)?nèi)容及分類，在軟件方法學(xué)的研究背景下，對(duì)形式化方法在軟件系統(tǒng)開(kāi)發(fā)每一個(gè)階段的應(yīng)用進(jìn)行了詳細(xì)分析和綜合評(píng)價(jià)。

關(guān)鍵詞：形式化方法;軟件方法學(xué);形式化的軟件開(kāi)發(fā)

早期軟件系統(tǒng)規(guī)模較小，20世紀(jì)60年代之前，對(duì)軟件系統(tǒng)的開(kāi)發(fā)一直通過(guò)“手工”方式，具有個(gè)人化及技藝化的開(kāi)發(fā)特點(diǎn)。60年代中期，計(jì)算機(jī)的容量和速度有了顯著提升，軟件系統(tǒng)規(guī)模越來(lái)越大，軟件開(kāi)發(fā)生產(chǎn)率不再能滿足現(xiàn)狀，軟件危機(jī)開(kāi)始爆發(fā)。60年代后期，針對(duì)“軟件危機(jī)”提出兩類解決辦法：一是將工程化應(yīng)用于軟件的開(kāi)發(fā)過(guò)程，即“軟件工程”的出現(xiàn)和發(fā)展;二是建立嚴(yán)格的理論基礎(chǔ)，采用形式化方法來(lái)指導(dǎo)軟件開(kāi)發(fā)過(guò)程。經(jīng)過(guò)近半個(gè)世紀(jì)的探索和應(yīng)用，形式化方法這一領(lǐng)域已經(jīng)取得了大量的研究成果。

1 形式化方法

軟件工程中的形式化方法就是通過(guò)嚴(yán)格的符號(hào)系統(tǒng)和數(shù)學(xué)模型來(lái)描述和驗(yàn)證一個(gè)目標(biāo)軟件系統(tǒng)的行為和特性，包括需求規(guī)格、設(shè)計(jì)和實(shí)現(xiàn)等。形式化方法所使用的是嚴(yán)格的數(shù)學(xué)語(yǔ)言，其語(yǔ)法和語(yǔ)義都是無(wú)二義的、精確的。形式化方法的研究主要集中在形式規(guī)約（Formal Specification）和建立在形式規(guī)約基礎(chǔ)上的形式驗(yàn)證（Formal Verification）兩個(gè)方面。

2 軟件方法學(xué)

2.1 軟件危機(jī)

60年代后期，軟件系統(tǒng)的規(guī)模逐步增大，程序?qū)崿F(xiàn)地復(fù)雜度也越來(lái)越高，可靠性問(wèn)題成為越來(lái)越多人關(guān)注的焦點(diǎn)。由于軟件開(kāi)發(fā)生產(chǎn)率不再能滿足計(jì)算機(jī)應(yīng)用迅速深入的趨勢(shì)，軟件危機(jī)開(kāi)始爆發(fā)。1968年北大西洋公約組織的計(jì)算機(jī)科學(xué)家在聯(lián)邦德國(guó)召開(kāi)國(guó)際會(huì)議，第一次討論軟件危機(jī)問(wèn)題，并正式提出“軟件工程”。

2.2 軟件方法學(xué)

近年來(lái)，國(guó)外出現(xiàn)了許多指導(dǎo)軟件開(kāi)發(fā)的方法?！败浖椒▽W(xué)”（Software Methodology）以軟件方法為研究對(duì)象，用來(lái)指導(dǎo)軟件設(shè)計(jì)的原理和原則，以及基于這些原理和原則的方法和技術(shù)。軟件方法學(xué)是“軟件工程”中的一個(gè)主要內(nèi)容。狹義的軟件方法學(xué)指某種特定的軟件設(shè)計(jì)指導(dǎo)規(guī)則和方法體系。軟件方法學(xué)的主要目的是高效地設(shè)計(jì)正確的軟件。根據(jù)性質(zhì)可分為以下兩類：

（1）形式化方法：形式方法通過(guò)精確的數(shù)學(xué)語(yǔ)言對(duì)系統(tǒng)的各類屬性和開(kāi)發(fā)過(guò)程做出嚴(yán)格的描述和驗(yàn)證，定義了如一致性、完全性、正確性、規(guī)約等概念。無(wú)需通過(guò)實(shí)際運(yùn)行來(lái)證明軟件規(guī)約是可實(shí)現(xiàn)的、建立的系統(tǒng)是可正確實(shí)現(xiàn)的、系統(tǒng)具有某些性質(zhì)等。

（2）非形式化方法：非形式方法則不考慮系統(tǒng)的嚴(yán)格性，通常采用文本、圖表等模型描述系統(tǒng)。

3 基于形式化方法的軟件開(kāi)發(fā)

3.1 形式化方法

（1）可行性分析：可行性分析是對(duì)待開(kāi)發(fā)系統(tǒng)提供一種綜合性的分析方法。綜合各方面因素論證待開(kāi)發(fā)系統(tǒng)是否可行，為開(kāi)發(fā)過(guò)程提出綜合評(píng)價(jià)和決策依據(jù)。由于形式化方法的符號(hào)演算系統(tǒng)仍不能完全表達(dá)自然語(yǔ)言，所以在此階段的應(yīng)用仍是一項(xiàng)巨大挑戰(zhàn)。

（2）需求分析：需求分析是在軟件開(kāi)發(fā)過(guò)程的早期階段，將用戶需求轉(zhuǎn)換為說(shuō)明文檔。一般非形式化的描述可能導(dǎo)致描述的不明確和需求的不一致，可能導(dǎo)致編程錯(cuò)誤，影響程序的使用和可靠性。形式化方法則要求明確描述用戶需求。

（3）體系結(jié)構(gòu)設(shè)計(jì)：體系結(jié)構(gòu)設(shè)計(jì)階段的根本目的是將用戶需求轉(zhuǎn)換為計(jì)算機(jī)可以實(shí)現(xiàn)的目標(biāo)系統(tǒng)。本階段側(cè)重描述軟件系統(tǒng)的接口、功能和結(jié)構(gòu)。形式化方法對(duì)于軟件需求描述的優(yōu)點(diǎn)同樣適用于軟件設(shè)計(jì)的描述。由于需求階段功能描述并不能完全實(shí)現(xiàn)，所以形式化方法在此階段的應(yīng)用仍存在問(wèn)題。使用者可采用半形式化方法來(lái)完成此階段的工作。

（4）詳細(xì)設(shè)計(jì)：詳細(xì)設(shè)計(jì)階段的形式化是以體系結(jié)構(gòu)規(guī)范為基礎(chǔ)進(jìn)行精化描述的過(guò)程。通過(guò)此階段的形式化描述能夠檢驗(yàn)需求描述和用戶需求是否一致。為使形式化方法更適用于詳細(xì)設(shè)計(jì)和精化過(guò)程，可將各種形式的規(guī)范聯(lián)系起來(lái)。

（5）編碼：自動(dòng)代碼生成器目前能將一些規(guī)模較小軟件系統(tǒng)的形式化描述直接轉(zhuǎn)換成可執(zhí)行程序。在簡(jiǎn)化軟件開(kāi)發(fā)過(guò)程的同時(shí)既節(jié)約了資源又增強(qiáng)了軟件的可靠性。

（6）測(cè)試發(fā)布：軟件開(kāi)發(fā)的最后階段是測(cè)試發(fā)布。在軟件投入運(yùn)行前，需要對(duì)軟件開(kāi)發(fā)各階段的文檔以及程序源代碼進(jìn)行檢查。對(duì)于測(cè)試來(lái)講，形式化方法可用于測(cè)試用例的自動(dòng)生成，保證測(cè)試用例的覆蓋率。

3.2 綜合評(píng)價(jià)

形式化方法開(kāi)發(fā)軟件系統(tǒng)的優(yōu)勢(shì)有：

（1）軟件開(kāi)發(fā)的基礎(chǔ)是對(duì)軟件需求的描述。形式化方法要求描述的明確性，很大程度上保證了需求的一致性，減少了可能的誤解，為正確實(shí)現(xiàn)用戶需求提供了更大的可能性。

（2）形式化驗(yàn)證對(duì)形式化描述的需求文檔提供明確的邏輯論證，通過(guò)推理驗(yàn)證來(lái)保證最終的軟件產(chǎn)品能夠滿足用戶需求。

（3）形式化描述和驗(yàn)證實(shí)現(xiàn)了系統(tǒng)的一致性分析和重復(fù)分析，提供了一個(gè)幾乎不依賴特定分析者的分析過(guò)程。

（4）形式化描述和驗(yàn)證基于計(jì)算機(jī)和嚴(yán)格符號(hào)系統(tǒng)的支持，實(shí)現(xiàn)了開(kāi)發(fā)和驗(yàn)證的自動(dòng)化，節(jié)約了人力資源并且保證了軟件的可靠性。

形式化方法開(kāi)發(fā)軟件系統(tǒng)的缺陷：

（1）形式化方法的使用建立在數(shù)學(xué)理論的基礎(chǔ)上，限制了大多數(shù)人員的學(xué)習(xí)和使用。

（2）缺乏一種通用的形式化方法來(lái)支持軟件生命周期每一階段。

（3）不同的數(shù)學(xué)規(guī)范在不同的模型和工程環(huán)境中可能不只有一種解釋，為形式驗(yàn)證帶來(lái)困難。

參考文獻(xiàn)：

[1]張廣泉.關(guān)于軟件形式化方法[J].重慶師范學(xué)院學(xué)報(bào)（自然科學(xué)版），2002（02）.

[2]張瑋瑋，陳珊.軟件開(kāi)發(fā)中的形式化方法介紹[J].張家口職業(yè)技術(shù)學(xué)院學(xué)報(bào)，2005，18（01）：54-57.

[3]陳丹.基于形式化方法的軟件開(kāi)發(fā)技術(shù)[J].軟件工程師，2009：52-53.

作者簡(jiǎn)介：熊小超（1992-），女，江西豐城人，研究生，研究方向：形式化方法。