3.1　軟件形式化測試技術概述

3.1.1　軟件形式化測試概述

形式化方法源于Dijkstra和Hoare的程序驗證。針對形式化方法的研究已經有幾十年，但目前仍沒有統一的對形式化方法的定義，Encyclopedia of Software Engineering一書對形式化方法的定義為：“用于開發計算機系統的形式化方法是基于數學的用于描述系統性質的技術。這樣的形式化方法提供了一個框架，人們可以在該框架中以系統的方式刻畫、開發和驗證系統。”通常，凡是采用嚴格的數學工具、具有精確數學語義的方法，都可以稱為形式化方法。形式化方法的一種分類方法如表3-1所示。

表3-1　形式化方法的一種分類方法

形式化方法在通信協議以及嵌入式軟件建模及測試中已取得較多研究成果，且已被越來越多地應用于安全關鍵軟件驗證領域。歐洲航天局和NASA對于安全關鍵軟件的開發高度推薦使用形式化方法。在實際應用中，實時嵌入式軟件往往是安全關鍵軟件，因此，在實時嵌入式軟件系統測試中采用形式化方法可以消除二義性，增強測試的準確性和一致性，提高測試的自動化程度和測試效率。

從國內外的技術發展和研究來看，目前基于形式化方法的軟件建模及測試技術的研究領域總結如圖3-1所示。

圖3-1　基于形式化方法的軟件建模及測試技術