軟件工程中的形式化方法研究

前言：想要寫出一篇引人入勝的文章？我們特意為您整理了軟件工程中的形式化方法研究范文，希望能給你帶來靈感和參考，敬請(qǐng)閱讀。

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

1形式化方法

1.1形式化方法

軟件工程中的形式化方法就是通過嚴(yán)格的符號(hào)系統(tǒng)和數(shù)學(xué)模型來描述和驗(yàn)證一個(gè)目標(biāo)軟件系統(tǒng)的行為和特性,包括需求規(guī)格、設(shè)計(jì)和實(shí)現(xiàn)等。形式化方法所使用的是嚴(yán)格的數(shù)學(xué)語言,其語法和語義都是無二義的、精確的。

1.2主要研究內(nèi)容

形式化方法的研究主要集中在形式規(guī)約(FormalSpecification)和建立在形式規(guī)約基礎(chǔ)上的形式驗(yàn)證(FormalVerification)兩個(gè)方面。形式規(guī)約是指通過具有精確語義的形式語言對(duì)程序功能進(jìn)行描述。描述結(jié)果將作為程序設(shè)計(jì)和驗(yàn)證的重要依據(jù)。形式驗(yàn)證是對(duì)現(xiàn)有的程序系統(tǒng)進(jìn)行驗(yàn)證,檢查其是否符合規(guī)約的要求。傳統(tǒng)的驗(yàn)證方式是通過實(shí)驗(yàn)對(duì)系統(tǒng)進(jìn)行查錯(cuò),包括模擬(simulation)和測(cè)試(testing)。

1.3形式化方法的分類

根據(jù)描述方式,可將形式化方法歸為兩類:

(1)模型描述的形式化方法。通過構(gòu)造一個(gè)數(shù)學(xué)模型來直接描述系統(tǒng)或程序。

(2)性質(zhì)描述的形式化方法。通過對(duì)目標(biāo)軟件系統(tǒng)中不同性質(zhì)的描述來間接描述系統(tǒng)或程序。根據(jù)表達(dá)能力,可將形式化方法大概分為五類[Barroca*1992]:

(1)模型方法——對(duì)系統(tǒng)狀態(tài)和改變系統(tǒng)狀態(tài)的動(dòng)作直接給出抽象定義,并進(jìn)行顯式描述。該方法的缺陷是不能顯式地表示并發(fā)。

(2)代數(shù)方法——通過定義不同操作的關(guān)系,隱式地描述操作。與模型方法相同,代數(shù)方法也不能顯式地表示并發(fā)。

(3)進(jìn)程代數(shù)方法——通過一個(gè)顯式模型來描述并發(fā)過程。將并發(fā)性歸結(jié)為非確定性,通過交錯(cuò)語義(interleavingsemantics)來表示系統(tǒng)行為。如:CCS,CSP,ACP等。

(4)邏輯方法——通過描述程序狀態(tài)規(guī)范和時(shí)間狀態(tài)規(guī)范的邏輯方法來描述系統(tǒng)特性,如:CTL,LTL。

(5)網(wǎng)絡(luò)模型方法——通過獨(dú)立描述網(wǎng)絡(luò)中的每一個(gè)節(jié)點(diǎn),顯式地給出系統(tǒng)的并發(fā)模型。如:Petri網(wǎng)。

2軟件方法學(xué)

2.1軟件危機(jī)

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

2.2軟件方法學(xué)

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

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

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

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

3.1形式化方法開發(fā)過程

按照軟件工程“自頂向下、逐步求精”的原則,軟件生命周期可分為六個(gè)階段:可行性分析、需求分析、體系結(jié)構(gòu)設(shè)計(jì)、詳細(xì)設(shè)計(jì)、編碼、測(cè)試,形式化方法貫穿軟件工程整個(gè)生命周期。

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

(2)需求分析:需求分析是在軟件開發(fā)過程的早期階段,將用戶需求轉(zhuǎn)換為說明文檔。一般非形式化的描述可能導(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)用仍存在問題。使用者可采用半形式化方法來完成此階段的工作。

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

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

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

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

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

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

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

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

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

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

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

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

作者：李婉璐 單位：寧夏大學(xué)數(shù)學(xué)計(jì)算機(jī)學(xué)院