3.1　軟件形式化測試技術(shù)概述

3.1.1　軟件形式化測試概述

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

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

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

從國內(nèi)外的技術(shù)發(fā)展和研究來看，目前基于形式化方法的軟件建模及測試技術(shù)的研究領(lǐng)域總結(jié)如圖3-1所示。

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