早期軟體系統規模較小,20世紀60年代之前,對軟體系統的開發一直通過「手工」方式,具有個人化及技藝化的開發特點。60年代中期,計算機的容量和速度有了顯著提升,軟體系統規模越來越大,軟體開發生產率不再能滿足現狀,軟體危機開始爆發。60年代後期,針對「軟體危機」提出兩類解決辦法:一是將工程化應用於軟體的開發過程,即「軟體工程」的出現和發展;二是建立嚴格的理論基礎,採用形式化方法來指導軟體開發過程。經過近半個世紀的探索和應用,形式化方法這一領域已經取得了大量的研究成果。
1形式化方法
1.1形式化方法
軟體工程中的形式化方法就是通過嚴格的符號系統和數學模型來描述和驗證一個目標軟體系統的行為和特性,包括需求規格、設計和實現等。形式化方法所使用的是嚴格的數學語言,其語法和語義都是無二義的、精確的。
1.2主要研究內容
形式化方法的研究主要集中在形式規約(FormalSpecification)和建立在形式規約基礎上的形式驗證(FormalVerification)兩個方面。形式規約是指通過具有精確語義的形式語言對程序功能進行描述。描述結果將作為程序設計和驗證的重要依據。形式驗證是對現有的程序系統進行驗證,檢查其是否符合規約的要求。傳統的驗證方式是通過實驗對系統進行查錯,包括模擬(simulation)和測試(testing)。
1.3形式化方法的分類
根據描述方式,可將形式化方法歸為兩類:
(1)模型描述的形式化方法。通過構造一個數學模型來直接描述系統或程序。
(2)性質描述的形式化方法。通過對目標軟體系統中不同性質的描述來間接描述系統或程序。根據表達能力,可將形式化方法大概分為五類[Barroca*1992]:
(1)模型方法——對系統狀態和改變系統狀態的動作直接給出抽象定義,並進行顯式描述。該方法的缺陷是不能顯式地表示並發。
(2)代數方法——通過定義不同操作的關係,隱式地描述操作。與模型方法相同,代數方法也不能顯式地表示並發。
(3)進程代數方法——通過一個顯式模型來描述並發過程。將並發性歸結為非確定性,通過交錯語義(interleavingsemantics)來表示系統行為。如:CCS,CSP,ACP等。
(4)邏輯方法——通過描述程序狀態規範和時間狀態規範的邏輯方法來描述系統特性,如:CTL,LTL。
(5)網絡模型方法——通過獨立描述網絡中的每一個節點,顯式地給出系統的並發模型。如:Petri網。
2軟體方法學
2.1軟體危機
60年代後期,軟體系統的規模逐步增大,程序實現地複雜度也越來越高,可靠性問題成為越來越多人關注的焦點。由於軟體開發生產率不再能滿足計算機應用迅速深入的趨勢,軟體危機開始爆發。1968年北大西洋公約組織的計算機科學家在聯邦德國召開國際會議,第一次討論軟體危機問題,並正式提出「軟體工程」。
2.2軟體方法學
近年來,國外出現了許多指導軟體開發的方法「。軟體方法學」(SoftwareMethodology)以軟體方法為研究對象,用來指導軟體設計的原理和原則,以及基於這些原理和原則的方法和技術。軟體方法學是「軟體工程」中的一個主要內容。狹義的軟體方法學指某種特定的軟體設計指導規則和方法體系。軟體方法學的主要目的是高效地設計正確的軟體。根據性質可分為以下兩類:
(1)形式化方法:形式方法通過精確的數學語言對系統的各類屬性和開發過程做出嚴格的描述和驗證,定義了如一致性、完全性、正確性、規約等概念。無需通過實際運行來證明軟體規約是可實現的、建立的系統是可正確實現的、系統具有某些性質等。
(2)非形式化方法:非形式方法則不考慮系統的嚴格性,通常採用文本、圖表等模型描述系統。
3基於形式化方法的軟體開發
3.1形式化方法開發過程
按照軟體工程「自頂向下、逐步求精」的原則,軟體生命周期可分為六個階段:可行性分析、需求分析、體系結構設計、詳細設計、編碼、測試,形式化方法貫穿軟體工程整個生命周期。
(1)可行性分析:可行性分析是對待開發系統提供一種綜合性的分析方法。綜合各方面因素論證待開發系統是否可行,為開發過程提出綜合評價和決策依據。由於形式化方法的符號演算系統仍不能完全表達自然語言,所在在此階段的應用仍是一項巨大挑戰。
(2)需求分析:需求分析是在軟體開發過程的早期階段,將用戶需求轉換為說明文檔。一般非形式化的描述可能導致描述的不明確和需求的不一致,可能導致編程錯誤,影響程序的使用和可靠性。形式化方法則要求明確描述用戶需求。
(3)體系結構設計:體系結構設計階段的根本目的是將用戶需求轉換為計算機可以實現的目標系統。本階段側重描述軟體系統的接口、功能和結構。形式化方法對於軟體需求描述的優點同樣適用於軟體設計的描述。由於需求階段功能描述並不能完全實現,所以形式化方法在此階段的應用仍存在問題。使用者可採用半形式化方法來完成此階段的工作。
(4)詳細設計:詳細設計階段的形式化是以體系結構規範為基礎進行精化描述的過程。通過此階段的形式化描述能夠檢驗需求描述和用戶需求是否一致。為使形式化方法更適用於詳細設計和精化過程,可將各種形式的規範聯繫起來。
(5)編碼:自動代碼生成器目前能將一些規模較小軟體系統的形式化描述直接轉換成可執行程序。在簡化軟體開發過程的同時既節約了資源又增強了軟體的可靠性。
(6)測試:軟體開發的最後階段是測試。在軟體投入運行前,需要對軟體開發各階段的文檔以及程序原始碼進行檢查。對於測試來講,形式化方法可用於測試用例的自動生成,保證測試用例的覆蓋率。
3.2綜合評價
形式化方法開發軟體系統的優勢有:
(1)軟體開發的基礎是對軟體需求的描述。形式化方法要求描述的明確性,很大程度上保證了需求的一致性,減少了可能的誤解,為正確實現用戶需求提供了更大的可能性。
(2)形式化驗證對形式化描述的需求文檔提供明確的邏輯論證,通過推理驗證來保證最終的軟體產品能夠滿足用戶需求。
(3)形式化描述和驗證實現了系統的一致性分析和重複分析,提供了一個幾乎不依賴特定分析者的分析過程。
(4)形式化描述和驗證基於計算機和嚴格符號系統的支持,實現了開發和驗證的自動化,節約了人力資源並且保證了軟體的可靠性。形式化方法開發軟體系統的缺陷:
(1)形式化方法的使用建立在數學理論的基礎上,限制了大多數人員的學習和使用。
(2)缺乏一種通用的形式化方法來支持軟體生命周期每一階段。
(3)不同的數學規範在不同的模型和工程環境中可能不只有一種解釋,為形式驗證帶來困難。
作者：李婉璐 單位：寧夏大學數學計算機學院
1形式化方法
1.1形式化方法
軟體工程中的形式化方法就是通過嚴格的符號系統和數學模型來描述和驗證一個目標軟體系統的行為和特性,包括需求規格、設計和實現等。形式化方法所使用的是嚴格的數學語言,其語法和語義都是無二義的、精確的。
1.2主要研究內容
形式化方法的研究主要集中在形式規約(FormalSpecification)和建立在形式規約基礎上的形式驗證(FormalVerification)兩個方面。形式規約是指通過具有精確語義的形式語言對程序功能進行描述。描述結果將作為程序設計和驗證的重要依據。形式驗證是對現有的程序系統進行驗證,檢查其是否符合規約的要求。傳統的驗證方式是通過實驗對系統進行查錯,包括模擬(simulation)和測試(testing)。
1.3形式化方法的分類
根據描述方式,可將形式化方法歸為兩類:
(1)模型描述的形式化方法。通過構造一個數學模型來直接描述系統或程序。
(2)性質描述的形式化方法。通過對目標軟體系統中不同性質的描述來間接描述系統或程序。根據表達能力,可將形式化方法大概分為五類[Barroca*1992]:
(1)模型方法——對系統狀態和改變系統狀態的動作直接給出抽象定義,並進行顯式描述。該方法的缺陷是不能顯式地表示並發。
(2)代數方法——通過定義不同操作的關係,隱式地描述操作。與模型方法相同,代數方法也不能顯式地表示並發。
(3)進程代數方法——通過一個顯式模型來描述並發過程。將並發性歸結為非確定性,通過交錯語義(interleavingsemantics)來表示系統行為。如:CCS,CSP,ACP等。
(4)邏輯方法——通過描述程序狀態規範和時間狀態規範的邏輯方法來描述系統特性,如:CTL,LTL。
(5)網絡模型方法——通過獨立描述網絡中的每一個節點,顯式地給出系統的並發模型。如:Petri網。
2軟體方法學
2.1軟體危機
60年代後期,軟體系統的規模逐步增大,程序實現地複雜度也越來越高,可靠性問題成為越來越多人關注的焦點。由於軟體開發生產率不再能滿足計算機應用迅速深入的趨勢,軟體危機開始爆發。1968年北大西洋公約組織的計算機科學家在聯邦德國召開國際會議,第一次討論軟體危機問題,並正式提出「軟體工程」。
2.2軟體方法學
近年來,國外出現了許多指導軟體開發的方法「。軟體方法學」(SoftwareMethodology)以軟體方法為研究對象,用來指導軟體設計的原理和原則,以及基於這些原理和原則的方法和技術。軟體方法學是「軟體工程」中的一個主要內容。狹義的軟體方法學指某種特定的軟體設計指導規則和方法體系。軟體方法學的主要目的是高效地設計正確的軟體。根據性質可分為以下兩類:
(1)形式化方法:形式方法通過精確的數學語言對系統的各類屬性和開發過程做出嚴格的描述和驗證,定義了如一致性、完全性、正確性、規約等概念。無需通過實際運行來證明軟體規約是可實現的、建立的系統是可正確實現的、系統具有某些性質等。
(2)非形式化方法:非形式方法則不考慮系統的嚴格性,通常採用文本、圖表等模型描述系統。
3基於形式化方法的軟體開發
3.1形式化方法開發過程
按照軟體工程「自頂向下、逐步求精」的原則,軟體生命周期可分為六個階段:可行性分析、需求分析、體系結構設計、詳細設計、編碼、測試,形式化方法貫穿軟體工程整個生命周期。
(1)可行性分析:可行性分析是對待開發系統提供一種綜合性的分析方法。綜合各方面因素論證待開發系統是否可行,為開發過程提出綜合評價和決策依據。由於形式化方法的符號演算系統仍不能完全表達自然語言,所在在此階段的應用仍是一項巨大挑戰。
(2)需求分析:需求分析是在軟體開發過程的早期階段,將用戶需求轉換為說明文檔。一般非形式化的描述可能導致描述的不明確和需求的不一致,可能導致編程錯誤,影響程序的使用和可靠性。形式化方法則要求明確描述用戶需求。
(3)體系結構設計:體系結構設計階段的根本目的是將用戶需求轉換為計算機可以實現的目標系統。本階段側重描述軟體系統的接口、功能和結構。形式化方法對於軟體需求描述的優點同樣適用於軟體設計的描述。由於需求階段功能描述並不能完全實現,所以形式化方法在此階段的應用仍存在問題。使用者可採用半形式化方法來完成此階段的工作。
(4)詳細設計:詳細設計階段的形式化是以體系結構規範為基礎進行精化描述的過程。通過此階段的形式化描述能夠檢驗需求描述和用戶需求是否一致。為使形式化方法更適用於詳細設計和精化過程,可將各種形式的規範聯繫起來。
(5)編碼:自動代碼生成器目前能將一些規模較小軟體系統的形式化描述直接轉換成可執行程序。在簡化軟體開發過程的同時既節約了資源又增強了軟體的可靠性。
(6)測試:軟體開發的最後階段是測試。在軟體投入運行前,需要對軟體開發各階段的文檔以及程序原始碼進行檢查。對於測試來講,形式化方法可用於測試用例的自動生成,保證測試用例的覆蓋率。
3.2綜合評價
形式化方法開發軟體系統的優勢有:
(1)軟體開發的基礎是對軟體需求的描述。形式化方法要求描述的明確性,很大程度上保證了需求的一致性,減少了可能的誤解,為正確實現用戶需求提供了更大的可能性。
(2)形式化驗證對形式化描述的需求文檔提供明確的邏輯論證,通過推理驗證來保證最終的軟體產品能夠滿足用戶需求。
(3)形式化描述和驗證實現了系統的一致性分析和重複分析,提供了一個幾乎不依賴特定分析者的分析過程。
(4)形式化描述和驗證基於計算機和嚴格符號系統的支持,實現了開發和驗證的自動化,節約了人力資源並且保證了軟體的可靠性。形式化方法開發軟體系統的缺陷:
(1)形式化方法的使用建立在數學理論的基礎上,限制了大多數人員的學習和使用。
(2)缺乏一種通用的形式化方法來支持軟體生命周期每一階段。
(3)不同的數學規範在不同的模型和工程環境中可能不只有一種解釋,為形式驗證帶來困難。
作者：李婉璐 單位：寧夏大學數學計算機學院
收藏