基于形式化方法的軟件開(kāi)發(fā)技術(shù)

摘要:形式化方法作為一種以數(shù)學(xué)為基礎(chǔ)的方法，能夠清晰、精確、抽象、簡(jiǎn)明地規(guī)范和驗(yàn)證軟件系統(tǒng)及其性質(zhì)，能夠極大地提高軟件的安全性和可靠性。本文從形式化方法的研究?jī)?nèi)容、分類(lèi)以及發(fā)展等方面出發(fā)，對(duì)基于形式化方法的軟件開(kāi)發(fā)的基本思想作了介紹，分析了使用形式化開(kāi)發(fā)軟件系統(tǒng)的優(yōu)勢(shì)和可靠性。

關(guān)鍵詞:管理信息系統(tǒng);本體;原型;實(shí)踐教學(xué)

1 引言

隨著軟件系統(tǒng)復(fù)雜度的不斷增長(zhǎng)，開(kāi)發(fā)正確、可靠的軟件，成為一個(gè)急待解決的問(wèn)題。解決此問(wèn)題的一個(gè)有前途、有希望的技術(shù)是形式化方法的應(yīng)用。形式化方法需要形式化規(guī)約說(shuō)明語(yǔ)言的支持。形式化方法建立在嚴(yán)格的數(shù)學(xué)基礎(chǔ)上，能夠清晰、精確、抽象、簡(jiǎn)明地規(guī)范和驗(yàn)證軟件系統(tǒng)及其性質(zhì)，其目標(biāo)是希望能使系統(tǒng)具有較高的可信度和正確性，并能使系統(tǒng)具有良好的結(jié)構(gòu)，使其易維護(hù)，關(guān)鍵是能較好地滿足用戶需求。

2 形式化方法的研究?jī)?nèi)容

形式化方法可以分為形式化描述和建立在形式化描述基礎(chǔ)之上的形式化開(kāi)發(fā)。形式化的描述就是用形式化的語(yǔ)言(具有嚴(yán)格的語(yǔ)法語(yǔ)義定義的語(yǔ)言)做描述。形式化的軟件開(kāi)發(fā)，就是用形式化的語(yǔ)言來(lái)描述軟件需求和特征，并且通過(guò)推理驗(yàn)證來(lái)保證最終的軟件產(chǎn)品是否滿足這些需求和具備這些特征。形式化方法研究的目的就是希望能夠提供更好的理論、方法和工具，擴(kuò)大形式化方法的應(yīng)用范圍和使用價(jià)值。

形式化方法的一個(gè)重要研究?jī)?nèi)容是形式規(guī)約(Formal Specification，也稱形式規(guī)范或形式化描述)，它是用具有精確語(yǔ)義的形式語(yǔ)言書(shū)寫(xiě)的程序功能描述，它是設(shè)計(jì)和編制程序的出發(fā)點(diǎn)，也是驗(yàn)證程序是否正確的依據(jù)。對(duì)形式規(guī)約通常要討論其一致性和完備性等性質(zhì)。形式規(guī)約的方法主要可分為兩類(lèi):一類(lèi)是面向模型的方法也稱為系統(tǒng)建模，該方法通過(guò)構(gòu)造系統(tǒng)的計(jì)算模型來(lái)刻畫(huà)系統(tǒng)的不同行為特征;另一類(lèi)是面向性質(zhì)的方法也稱為性質(zhì)描述，該方法通過(guò)定義系統(tǒng)必須滿足的一些性質(zhì)來(lái)描述一個(gè)系統(tǒng)。不同的形式規(guī)約方法要求不同的形式規(guī)約語(yǔ)言，即用于書(shū)寫(xiě)形式規(guī)約的語(yǔ)言(也稱形式化描述語(yǔ)言)。形式驗(yàn)證形式化方法的另一重要研究?jī)?nèi)容是形式驗(yàn)證(Formal Verification)。形式驗(yàn)證與形式規(guī)約之間具有緊密的聯(lián)系，形式驗(yàn)證就是驗(yàn)證已有的程序系統(tǒng)是否滿足其規(guī)約的要求，它也是形式化方法所要解決的核心問(wèn)題。傳統(tǒng)的驗(yàn)證方法包括模擬(simulation)和測(cè)試(testing)，它們都是通過(guò)實(shí)驗(yàn)的方法對(duì)系統(tǒng)進(jìn)行查錯(cuò)。

3 形式化方法的分類(lèi)

根據(jù)說(shuō)明目標(biāo)軟件系統(tǒng)的方式，形式化方法可以分為兩類(lèi):

(1)面向模型的形式化方法。面向模型的方法通過(guò)構(gòu)造一個(gè)數(shù)學(xué)模型來(lái)說(shuō)明系統(tǒng)的行為。

(2)面向?qū)傩缘男问交椒āＣ嫦驅(qū)傩缘姆椒ㄍㄟ^(guò)描述目標(biāo)軟件系統(tǒng)的各種屬性來(lái)間接定義系統(tǒng)行為。

根據(jù)表達(dá)能力，形式化方法可以分為五類(lèi):

(1)基于模型的方法:通過(guò)明確定義狀態(tài)和操作來(lái)建立一個(gè)系統(tǒng)模型(使系統(tǒng)從一個(gè)狀態(tài)轉(zhuǎn)換到另一個(gè)狀態(tài))。

(2)基于邏輯的方法:用邏輯描述系統(tǒng)預(yù)期的性能，包括底層規(guī)約、時(shí)序和可能性行為。采用與所選邏輯相關(guān)的公理系統(tǒng)證明系統(tǒng)具有預(yù)期的性能。用具體的編程構(gòu)造擴(kuò)充邏輯從而得到一種廣譜形式化方法，通過(guò)保持正確性的細(xì)化步驟集來(lái)開(kāi)發(fā)系統(tǒng)。

(3)代數(shù)方法:通過(guò)將未定義狀態(tài)下不同的操作行為相聯(lián)系，給出操作的顯式定義。與基于模型的方法相同的是，沒(méi)有給出并發(fā)的顯式表示。

(4)過(guò)程代數(shù)方法:通過(guò)限制所有容許的可觀察的過(guò)程間通信來(lái)表示系統(tǒng)行為。此類(lèi)方法允許并發(fā)過(guò)程的顯式表示。

(5)基于網(wǎng)絡(luò)的方法:由于圖形化表示法易于理解，而且非專業(yè)人員能夠使用，因此是一種通用的系統(tǒng)確定表示法。該方法采用具有形式語(yǔ)義的圖形語(yǔ)言，為系統(tǒng)開(kāi)發(fā)和再工程帶來(lái)特殊的好處。

4 形式化方法在軟件開(kāi)發(fā)中的應(yīng)用

基于形式化方法的軟件開(kāi)發(fā)的基本思想是:用形式化規(guī)約語(yǔ)言精確地描述軟件規(guī)約說(shuō)明，然后由支持形式化的工具完全自動(dòng)化或半自動(dòng)化地轉(zhuǎn)化為可執(zhí)行代碼。形式化方法在軟件開(kāi)發(fā)中能夠起到的作用是多方面的。形式化方法的優(yōu)勢(shì)對(duì)于軟件要求的描述同樣適用于軟件設(shè)計(jì)的描述。

4.1 需求分析

需求分析用戶的需求從初始概念轉(zhuǎn)換為需求文檔，需求文檔是與用戶交流思想的主要基礎(chǔ)。在需求階段使用形式化方法將會(huì)更加完善形式化方法已知的益處，形式化方法中的符號(hào)系統(tǒng)將會(huì)變得更全面、更完整，它不僅能描述功能性的需求，而且亦能描述非功能性的需求。

4.2 系統(tǒng)規(guī)范

系統(tǒng)規(guī)范階段主要描述系統(tǒng)而不涉及環(huán)境，這對(duì)于使用代數(shù)規(guī)范技術(shù)非常有利，它采用輸入、輸出間的關(guān)系來(lái)描述系統(tǒng)的行為。在此階段，可以應(yīng)用兩種可能的形式技術(shù):一個(gè)是發(fā)展代數(shù)技術(shù)以使其可應(yīng)用于大型系統(tǒng)的規(guī)范(尚未見(jiàn)到代數(shù)規(guī)范應(yīng)用于大型系統(tǒng)中的實(shí)例)，這就要求此技術(shù)能將規(guī)范模塊化;另一個(gè)是可能在技術(shù)上找到一條可以減少設(shè)計(jì)自由度的途徑。

4.3 體系結(jié)構(gòu)設(shè)計(jì)

體系結(jié)構(gòu)設(shè)計(jì)階段描述系統(tǒng)的接口、功能、結(jié)構(gòu)的初步實(shí)現(xiàn)。在此階段應(yīng)用形式化方法的主要問(wèn)題是，沒(méi)有能夠完成需求階段所有工作的方法或符號(hào)系統(tǒng)。目前，形式化方法的使用者必須選擇適合其應(yīng)用領(lǐng)域特點(diǎn)的方法，或使用一種折衷的方法，從不同的形式化方法中找到一個(gè)合適的方法來(lái)完成此階段的工作。

4.4 詳細(xì)設(shè)計(jì)

詳細(xì)設(shè)計(jì)是由體系結(jié)構(gòu)規(guī)范出發(fā)的精化過(guò)程。精化可以使我們定義和驗(yàn)證同一系統(tǒng)的兩個(gè)描述之間關(guān)系的正確性、一致性。詳細(xì)設(shè)計(jì)中的保持結(jié)構(gòu)觀點(diǎn)與目前的精化技術(shù)是一致的，為使形式化方法能夠應(yīng)用于詳細(xì)設(shè)計(jì)和精化過(guò)程，有必要采用一種折衷的方法，基于一種特殊的基礎(chǔ)，研究如何將各種形式的(Formal and Informal)規(guī)范聯(lián)系起來(lái)。

4.5 實(shí)現(xiàn)

在此階段，已有大量的關(guān)于形式處理的工作，即將程序與其的規(guī)范形式地對(duì)應(yīng)起來(lái)。形式實(shí)現(xiàn)技術(shù)在順序程序上應(yīng)用較廣，目前也有對(duì)并發(fā)程序方面的研究。若要使形式實(shí)現(xiàn)技術(shù)能廣泛地應(yīng)用，還須對(duì)其做較大的改進(jìn)，以提高其效率，降低其使用代價(jià)。

5 使用形式化開(kāi)發(fā)軟件系統(tǒng)的主要優(yōu)勢(shì)

軟件開(kāi)發(fā)自動(dòng)化技術(shù)是提高軟件生產(chǎn)率的根本途徑之一。軟件自動(dòng)化的前提是形式化，形式化不僅僅是對(duì)用戶需求，而且也是對(duì)整個(gè)軟件系統(tǒng)的嚴(yán)格定義。使用形式化方法可以克服傳統(tǒng)的軟件開(kāi)發(fā)方法的缺點(diǎn)。具體來(lái)說(shuō)，使用形式化開(kāi)發(fā)軟件系統(tǒng)的主要優(yōu)勢(shì)有:

(1)形式化說(shuō)明以邏輯精確性為特色， 除去了在非形式化說(shuō)明中不可避免的大部分含糊不清的描述，這種精確性為開(kāi)發(fā)人員與用戶對(duì)需求的一致性理解， 及需求的正確執(zhí)行提供了更大的可能性。

(2)形式化證明通過(guò)對(duì)需求分析中所描述的系統(tǒng)行為提供邏輯的精確論證， 除去了需求分析中的模糊性和主觀性。

(3)通過(guò)形式化說(shuō)明和證明實(shí)現(xiàn)了系統(tǒng)的重復(fù)分析、一致性分析以及一個(gè)較少依賴特定分析者技術(shù)和毅力的分析過(guò)程。

(4)形式化說(shuō)明和證明可以通過(guò)“裁剪”以適合于給定的項(xiàng)目及技術(shù)要求， 也就是說(shuō)能被調(diào)整以滿足具體項(xiàng)目的需要。

(5)形式化說(shuō)明和證明能夠應(yīng)用于任何開(kāi)發(fā)階段，包括目前最需要分析方法的開(kāi)發(fā)早期，越早發(fā)現(xiàn)和確定錯(cuò)誤比晚一些發(fā)現(xiàn)付出的代價(jià)要小的多。

(6)形式化說(shuō)明和證明是基于計(jì)算機(jī)的工具所支持，這使得一致性檢查和證明等實(shí)現(xiàn)了自動(dòng)化，提高了系統(tǒng)的可靠性，減少了在分析方面的費(fèi)用。同時(shí)，這些工具容許證明能夠被重復(fù)執(zhí)行而大大增強(qiáng)了分析的重復(fù)性。

(7)形式化說(shuō)明和證明彌補(bǔ)了現(xiàn)有的測(cè)試方法， 通過(guò)提供一個(gè)精確的形式化說(shuō)明而得以獲取一個(gè)好的測(cè)試計(jì)劃。

參考文獻(xiàn)

[1]鄭紅軍，張乃孝.軟件開(kāi)發(fā)中的形式化方法[J].北京大學(xué)學(xué)報(bào)，2005.

[2]吳會(huì)松.一種以面向?qū)ο蠹靶问交夹g(shù)為基礎(chǔ)的嚴(yán)格的軟件開(kāi)發(fā)方法[J].鄭州工業(yè)大學(xué)學(xué)報(bào)，1997(3).

[3]羅蜜，張為群.結(jié)合形式化方法的系統(tǒng)開(kāi)發(fā)[J].西南師范大學(xué)學(xué)報(bào)，2003(4).

[4]試論軟件的可靠性及其保證[J].軟件世界，2004(10).