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

陳　丹

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

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

1 引言

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

2 形式化方法的研究內(nèi)容

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

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

3 形式化方法的分類

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

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

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

根據(jù)表達能力,形式化方法可以分為五類:

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

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

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

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

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

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

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

4.1 需求分析

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

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

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

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

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

4.4 詳細設(shè)計

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

4.5 實現(xiàn)

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

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

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

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

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

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

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

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

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

(7)形式化說明和證明彌補了現(xiàn)有的測試方法, 通過提供一個精確的形式化說明而得以獲取一個好的測試計劃。

參考文獻

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

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

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

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