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

摘 要：軟件工程中的形式化方法是以數學理論為基礎，建立的一種用來解決軟件工程領域問題的系統性分析方法。形式化方法通過具有明確語義的形式語言來描述目標軟件系統的行為和特征，為目標系統開發提供了一個模型化的有效設計和分析途徑，保障了系統的安全性和可靠性。本文簡單介紹了形式化方法的研究內容及分類，在軟件方法學的研究背景下，對形式化方法在軟件系統開發每一個階段的應用進行了詳細分析和綜合評價。

關鍵詞：形式化方法;軟件方法學;形式化的軟件開發

早期軟件系統規模較小，20世紀60年代之前，對軟件系統的開發一直通過“手工”方式，具有個人化及技藝化的開發特點。60年代中期，計算機的容量和速度有了顯著提升，軟件系統規模越來越大，軟件開發生產率不再能滿足現狀，軟件危機開始爆發。60年代后期，針對“軟件危機”提出兩類解決辦法：一是將工程化應用于軟件的開發過程，即“軟件工程”的出現和發展;二是建立嚴格的理論基礎，采用形式化方法來指導軟件開發過程。經過近半個世紀的探索和應用，形式化方法這一領域已經取得了大量的研究成果。

1 形式化方法

軟件工程中的形式化方法就是通過嚴格的符號系統和數學模型來描述和驗證一個目標軟件系統的行為和特性，包括需求規格、設計和實現等。形式化方法所使用的是嚴格的數學語言，其語法和語義都是無二義的、精確的。形式化方法的研究主要集中在形式規約（Formal Specification）和建立在形式規約基礎上的形式驗證（Formal Verification）兩個方面。

2 軟件方法學

2.1 軟件危機

60年代后期，軟件系統的規模逐步增大，程序實現地復雜度也越來越高，可靠性問題成為越來越多人關注的焦點。由于軟件開發生產率不再能滿足計算機應用迅速深入的趨勢，軟件危機開始爆發。1968年北大西洋公約組織的計算機科學家在聯邦德國召開國際會議，第一次討論軟件危機問題，并正式提出“軟件工程”。

2.2 軟件方法學

近年來，國外出現了許多指導軟件開發的方法。“軟件方法學”（Software Methodology）以軟件方法為研究對象，用來指導軟件設計的原理和原則，以及基于這些原理和原則的方法和技術。軟件方法學是“軟件工程”中的一個主要內容。狹義的軟件方法學指某種特定的軟件設計指導規則和方法體系。軟件方法學的主要目的是高效地設計正確的軟件。根據性質可分為以下兩類：

（1）形式化方法：形式方法通過精確的數學語言對系統的各類屬性和開發過程做出嚴格的描述和驗證，定義了如一致性、完全性、正確性、規約等概念。無需通過實際運行來證明軟件規約是可實現的、建立的系統是可正確實現的、系統具有某些性質等。

（2）非形式化方法：非形式方法則不考慮系統的嚴格性，通常采用文本、圖表等模型描述系統。

3 基于形式化方法的軟件開發

3.1 形式化方法

（1）可行性分析：可行性分析是對待開發系統提供一種綜合性的分析方法。綜合各方面因素論證待開發系統是否可行，為開發過程提出綜合評價和決策依據。由于形式化方法的符號演算系統仍不能完全表達自然語言，所以在此階段的應用仍是一項巨大挑戰。

（2）需求分析：需求分析是在軟件開發過程的早期階段，將用戶需求轉換為說明文檔。一般非形式化的描述可能導致描述的不明確和需求的不一致，可能導致編程錯誤，影響程序的使用和可靠性。形式化方法則要求明確描述用戶需求。

（3）體系結構設計：體系結構設計階段的根本目的是將用戶需求轉換為計算機可以實現的目標系統。本階段側重描述軟件系統的接口、功能和結構。形式化方法對于軟件需求描述的優點同樣適用于軟件設計的描述。由于需求階段功能描述并不能完全實現，所以形式化方法在此階段的應用仍存在問題。使用者可采用半形式化方法來完成此階段的工作。

（4）詳細設計：詳細設計階段的形式化是以體系結構規范為基礎進行精化描述的過程。通過此階段的形式化描述能夠檢驗需求描述和用戶需求是否一致。為使形式化方法更適用于詳細設計和精化過程，可將各種形式的規范聯系起來。

（5）編碼：自動代碼生成器目前能將一些規模較小軟件系統的形式化描述直接轉換成可執行程序。在簡化軟件開發過程的同時既節約了資源又增強了軟件的可靠性。

（6）測試發布：軟件開發的最后階段是測試發布。在軟件投入運行前，需要對軟件開發各階段的文檔以及程序源代碼進行檢查。對于測試來講，形式化方法可用于測試用例的自動生成，保證測試用例的覆蓋率。

3.2 綜合評價

形式化方法開發軟件系統的優勢有：

（1）軟件開發的基礎是對軟件需求的描述。形式化方法要求描述的明確性，很大程度上保證了需求的一致性，減少了可能的誤解，為正確實現用戶需求提供了更大的可能性。

（2）形式化驗證對形式化描述的需求文檔提供明確的邏輯論證，通過推理驗證來保證最終的軟件產品能夠滿足用戶需求。

（3）形式化描述和驗證實現了系統的一致性分析和重復分析，提供了一個幾乎不依賴特定分析者的分析過程。

（4）形式化描述和驗證基于計算機和嚴格符號系統的支持，實現了開發和驗證的自動化，節約了人力資源并且保證了軟件的可靠性。

形式化方法開發軟件系統的缺陷：

（1）形式化方法的使用建立在數學理論的基礎上，限制了大多數人員的學習和使用。

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

（3）不同的數學規范在不同的模型和工程環境中可能不只有一種解釋，為形式驗證帶來困難。

參考文獻：

[1]張廣泉.關于軟件形式化方法[J].重慶師范學院學報（自然科學版），2002（02）.

[2]張瑋瑋，陳珊.軟件開發中的形式化方法介紹[J].張家口職業技術學院學報，2005，18（01）：54-57.

[3]陳丹.基于形式化方法的軟件開發技術[J].軟件工程師，2009：52-53.

作者簡介：熊小超（1992-），女，江西豐城人，研究生，研究方向：形式化方法。