形式化軟件開發(fā)方法 PPT課件

1、形式化軟件開發(fā)方法,第三組 2111301155 李林鋼,1,形式化方法的含義,從廣義上講，形式化方法是借助數(shù)學(xué)的方法來解決軟件工程領(lǐng)域的問題，主要包括建立精確的數(shù)學(xué)模型以及對模型的分析活動(dòng)。 狹義的講，形式化方法是運(yùn)用形式化語言，進(jìn)行形式化的規(guī)格描述、模型推理和驗(yàn)證的方法。,2,形式化方法的含義,就形式化建模而言，形式化表示必須包含一組定義其語法語義的形式化規(guī)則。這些規(guī)則可用于分析給定的表達(dá)式是否符合語法規(guī)定，或證明該表達(dá)式具有某種性質(zhì)。,3,形式化方法的出發(fā)點(diǎn),形式化方法的出發(fā)點(diǎn)是數(shù)學(xué)邏輯方法，其目的是開發(fā)可靠的軟件產(chǎn)品。 從軟件開發(fā)來講，形式化方法目前并非軟件開發(fā)的主流。從軟件發(fā)展看，早

2、期的軟件是用于數(shù)值計(jì)算，程序語言側(cè)重于函數(shù)和算法的描述，后來數(shù)據(jù)庫的應(yīng)用和數(shù)據(jù)結(jié)構(gòu)逐漸變得重要。現(xiàn)在的軟件更為復(fù)雜，因此，對象、組件、接口、通訊、開放等成為非常重要的概念。 從軟件工程方法來講，有一套描述這些概念的辦法，比如說用圖形、表格、邏輯、自然語言等，交叉使用以描述一個(gè)系統(tǒng)的各個(gè)方面。因此換一個(gè)角度來考慮，我們也可以以目前常用的軟件開發(fā)方法為出發(fā)點(diǎn)，研究怎樣將這些方法形式化，使軟件系統(tǒng)的描述精確化，以減少可能的誤解所帶來的問題；或以目前常用的軟件開發(fā)過程為出發(fā)點(diǎn)，研究怎樣在軟件開發(fā)過程中增加一些形式化方法的應(yīng)用，以提高軟件的可靠性。,4,形式化方法的分類,形式化方法可以分為形式化描述和建

3、立在形式化描述基礎(chǔ)之上的形式化開發(fā)。 形式化的描述就是用形式化的語言(具有嚴(yán)格的語法語義定義的語言，如流程圖，petri網(wǎng)等)做描述。 形式化的軟件開發(fā)，就是用形式化的語言來描述軟件需求和特征，并且通過推理驗(yàn)證來保證最終的軟件產(chǎn)品是否滿足這些需求和具備這些特征。 這樣的驗(yàn)證當(dāng)然得建立在嚴(yán)格的語法語義的基礎(chǔ)之上的。在實(shí)際應(yīng)用中，這是不容易做到的。形式化方法研究的目的就是希望能夠提供更好的理論、方法和工具，擴(kuò)大形式化方法的應(yīng)用范圍和使用價(jià)值。,5,形式化方法的意義,形式化方法的意義在于它能幫助發(fā)現(xiàn)其它方法不容易發(fā)現(xiàn)的系統(tǒng)描述的不一致、不明確或不完整，有助于增加軟件開發(fā)人員對系統(tǒng)的理解，因此形式化方

4、法是提高軟件系統(tǒng)，特別是Safety-Critical系統(tǒng)的安全性與可靠性的重要手段。最早的形式化方法是邏輯與邏輯推理，它的目標(biāo)是使推理機(jī)械化。 從廣義上講，這一目標(biāo)受到許多挫折，比如說邏輯系統(tǒng)的不完備性(incompleteness)、邏輯系統(tǒng)的不可判定性(undecidability)、自動(dòng)推理的難處理性(intractability)。但是在一些實(shí)際應(yīng)用上，邏輯方法和自動(dòng)推理還是起著非常大的作用。,6,形式化方法的作用,形式化方法在軟件開發(fā)中能夠起到的作用是多方面的。 首先是對軟件需求的描述，軟件需求的描述是軟件開發(fā)的基礎(chǔ)。比如說一般非形式化的描述很可能導(dǎo)致描述的不明確和不一致，如果描述

5、的不明確和不一致將導(dǎo)致設(shè)計(jì)、編程的錯(cuò)誤，將來的修改所要付出的代價(jià)就非常大了，如果導(dǎo)致的錯(cuò)誤沒有被發(fā)現(xiàn)，則影響程序的可靠和使用。形式化方法則要求描述的明確性，而描述的不一致性也就相對易于發(fā)現(xiàn)。,7,形式化方法的作用,其次是對軟件設(shè)計(jì)的描述。軟件設(shè)計(jì)的描述和軟件需求的描述一樣重要，形式化方法的優(yōu)點(diǎn)對于軟件需求的描述同樣適用于軟件設(shè)計(jì)的描述，另外由于有了軟件需求的形式化描述，我們可以檢驗(yàn)軟件的設(shè)計(jì)是否滿足軟件的要求。 對于編程來講，我們可以考慮自動(dòng)代碼生成。對于一些簡單的系統(tǒng)，形式化的描述有可能直接轉(zhuǎn)換成可執(zhí)行程序，這就簡化了軟件開發(fā)過程，節(jié)約了資源和減少了出錯(cuò)的可能性。另外，形式化方法可以用于程序

6、的驗(yàn)證，以保證程序的正確性。 對于測試來講，形式化方法可用于測試用例的自動(dòng)生成，這可以節(jié)約許多時(shí)間和在一定程度上保證測試用例的覆蓋率。,8,形式化方法的爭議和缺陷,形式化方法中所包含的數(shù)學(xué)理論，限制了大多數(shù)程序設(shè)計(jì)人員的學(xué)習(xí)和使用； 認(rèn)為采用形式化方法會(huì)延誤項(xiàng)目開發(fā)周期、增加開發(fā)費(fèi)用； 許多流行的形式化方法對于較小規(guī)模的項(xiàng)目是有效的，但卻很難應(yīng)用于一些大型系統(tǒng)； 形式化方法不能確保開發(fā)出完全正確的軟件； 缺乏對軟件生命周期內(nèi)各個(gè)階段提供全面支持的形式化方法；,9,形式化方法的描述方式,形式化方法原則上就是用數(shù)學(xué)與邏輯的方法描述和驗(yàn)證軟件。 從描述上講，一方面是系統(tǒng)或程序的描述，另一方面是性質(zhì)的

7、描述。 這些可以用一種或多種語言來描述。這些語言包括命題邏輯，一階邏輯，高階邏輯，代數(shù)，狀態(tài)機(jī)，并發(fā)狀態(tài)機(jī)，自動(dòng)機(jī)，計(jì)算樹邏輯，線性時(shí)序邏輯，進(jìn)程代數(shù)， -演算， -演算，特殊的程序語言，以及程序語言的子集等。,10,形式化方法的描述方式,從驗(yàn)證來講，主要有兩類方法，一類是以邏輯推理為基礎(chǔ)，另一類則以窮盡搜索為基礎(chǔ)。 邏輯推理有 natural deduction, sequent calculus, resolution 以及Hoare-logic 等方法。 窮盡搜索方法統(tǒng)稱為模型檢測。這類方法與系統(tǒng)或程序以及系統(tǒng)性質(zhì)的表示有很大的關(guān)系，比如說符號模型檢測，其基本原理是用命題邏輯公式表示狀態(tài)

8、轉(zhuǎn)換關(guān)系，用不動(dòng)點(diǎn)算法計(jì)算狀態(tài)的可達(dá)性以及這些狀態(tài)是否滿足某些性質(zhì)。,11,12,軟件形式化方法的研究方向,(1) 基礎(chǔ)概念：復(fù)合、抽象、重用模型、數(shù)學(xué)理論組合、數(shù)據(jù)結(jié)構(gòu)及算法。 (2) 形式化方法與面向?qū)ο蠓椒ǖ慕Y(jié)合：這方面的研究體現(xiàn)在兩個(gè)方面：利用面向?qū)ο蠼Y(jié)構(gòu)來提高形式符號的表達(dá)能力；使用形式化方法來分析面向?qū)ο蟮恼Z義或提高這些標(biāo)記符號的表達(dá)對象概念的能力。 (3) 工具開發(fā)：具有良好用戶界面、易于學(xué)習(xí)和操作簡單的形式化方法支撐工具（如原型開發(fā)工具Axure），對于形式化方法的推廣應(yīng)用是大有裨益的。追求通用的完善的形式化方法及其支撐工具是不現(xiàn)實(shí)的，側(cè)重于如下某一個(gè)或幾個(gè)方面準(zhǔn)則的特色方法和

9、工具是未來研究的重點(diǎn)。,13,關(guān)于形式化方法的幾點(diǎn)建議及發(fā)展方向,基于上面對形式化方法的分析和討論，我們提出對形式化方法的幾點(diǎn)可能的改進(jìn)，從而也就確定了形式化方法的一些發(fā)展方向。 可重用的規(guī)范庫及更易接受的符號系統(tǒng)將更有助于形式化方法的研究與應(yīng)用。在這方面，目前也有一些研究成果；對可重用規(guī)范的研究目前較少。當(dāng)然，這一改進(jìn)工作并不是短期內(nèi)可以完成的。 改進(jìn)形式規(guī)范的語法、語義定義的質(zhì)量，從而可以使得形式化方法更加“穩(wěn)定”。 加強(qiáng)規(guī)范語言中對并發(fā)控制和容錯(cuò)處理的表達(dá)能力，同時(shí)也要使精化技術(shù)能夠處理這類并發(fā)機(jī)制和容錯(cuò)。這方面的改進(jìn)也是長期的研究課題。 對于支持形式化方法的工具的可信度問題，一直是困擾形式