軟件形式化方法是指建立在嚴(yán)格數(shù)學(xué)基礎(chǔ)上的軟件開(kāi)發(fā)方法。形式化方法模型的主要活動(dòng)是生成計(jì)算機(jī)軟件形式化的數(shù)學(xué)規(guī)格說(shuō)明。形式化方法使軟件開(kāi)發(fā)人員可以應(yīng)用嚴(yán)格的數(shù)學(xué)符號(hào)來(lái)說(shuō)明、開(kāi)發(fā)和驗(yàn)證基于計(jì)算機(jī)的系統(tǒng)。

起源

軟件形式化方法最早可追溯到20世紀(jì)50年代后期對(duì)于程序設(shè)計(jì)語(yǔ)言編譯技術(shù)的研究，即J.Backus提出BNF描述Algol60語(yǔ)言的語(yǔ)法，出現(xiàn)了各 種語(yǔ)法分析程序自動(dòng)生成器以及語(yǔ)法制導(dǎo)的編譯方法，使得編譯系統(tǒng)的開(kāi)發(fā)從“手工藝制作方式”發(fā)展成具有牢固理論基礎(chǔ)的系統(tǒng)方法。

形式化方法的研究高潮始于20世紀(jì)60年代后期，針對(duì)當(dāng)時(shí)所謂“軟件危機(jī)”,人們提出種種解決方法，歸納起來(lái)有兩類(lèi)：一是采用工程方法來(lái)組織、管理軟件的開(kāi)發(fā)過(guò)程；二是深入探討程 序和程序開(kāi)發(fā)過(guò)程的規(guī)律，建立嚴(yán)密的理論，以其用來(lái)指導(dǎo)軟件開(kāi)發(fā)實(shí)踐。前者導(dǎo)致“軟件工程”的出現(xiàn)和發(fā)展，后者則推動(dòng)了形式化方法的深入研究。經(jīng)過(guò)30多 年的研究和應(yīng)用，如今人們?cè)谛问交椒ㄟ@一領(lǐng)域取得了大量、重要的成果，從早期最簡(jiǎn)單的形式化方法一階謂詞演算方法到現(xiàn)在的應(yīng)用于不同領(lǐng)域、不同階段的基于邏輯、狀態(tài)機(jī)、網(wǎng)絡(luò)、進(jìn)程代數(shù)、代數(shù)等眾多形式化方法。形式化方法的發(fā)展趨勢(shì)逐漸融入軟件開(kāi)發(fā)過(guò)程的各個(gè)階段，從需求分析、功能描述(規(guī)約)、(體系結(jié)構(gòu)/算法)設(shè)計(jì)、編程、測(cè)試直至維護(hù)。

內(nèi)容

形式化方法的本質(zhì)是基于數(shù)學(xué)的方法來(lái)描述目標(biāo)軟件系統(tǒng)屬性的一種技術(shù)。不同的形式化方法的數(shù)學(xué)基礎(chǔ)是不同的，有的以集合論和一階謂詞演算為基礎(chǔ)（如Z和VDM），有的則以時(shí)態(tài)邏輯為基礎(chǔ)。形式化方法需要形式化規(guī)約說(shuō)明語(yǔ)言的支持。

這樣的形式化方法提供了一個(gè)框架，可以在框架中以系統(tǒng)的而不是特別的方式刻劃、開(kāi)發(fā)和驗(yàn)證系統(tǒng)。如果一個(gè)方法有良好的數(shù)學(xué)基礎(chǔ)，那么它就是形式化的，典型地以形式化規(guī)約語(yǔ)言給出。這個(gè)基礎(chǔ)提供一系列精確定義的概念，如：一致性和完整性，以及定義規(guī)范的實(shí)現(xiàn)和正確性。這種方法的一個(gè)變型是凈室軟件工程（cleanroom software engineering），這一軟件工程方法目前已應(yīng)用于一些軟件開(kāi)發(fā)機(jī)構(gòu)。

分類(lèi)

1、根據(jù)說(shuō)明目標(biāo)軟件系統(tǒng)的方式，形式化方法可以分為兩類(lèi)：

1.面向模型的形式化方法。面向模型的方法通過(guò)構(gòu)造一個(gè)數(shù)學(xué)模型來(lái)說(shuō)明系統(tǒng)的行為。

2.面向?qū)傩缘男问交椒?。面向?qū)傩缘姆椒ㄍㄟ^(guò)描述目標(biāo)軟件系統(tǒng)的各種屬性來(lái)間接定義系統(tǒng)行為。

2、根據(jù)表達(dá)能力，形式化方法可以分為五類(lèi)：

1）基于模型的方法：通過(guò)明確定義狀態(tài)和操作來(lái)建立一個(gè)系統(tǒng)模型（使系統(tǒng)從一個(gè)狀態(tài)轉(zhuǎn)換到另一個(gè)狀態(tài)）。用這種方法雖可以表示非功能性需求（諸如時(shí)間需求），但不能很好地表示并發(fā)性。如：Z語(yǔ)言，VDM，B方法等。

2）基于邏輯的方法：用邏輯描述系統(tǒng)預(yù)期的性能，包括底層規(guī)約、時(shí)序和可能性行為。采用與所選邏輯相關(guān)的公理系統(tǒng)證明系統(tǒng)具有預(yù)期的性能。用具體的編程構(gòu) 造擴(kuò)充邏輯從而得到一種廣譜形式化方法，通過(guò)保持正確性的細(xì)化步驟集來(lái)開(kāi)發(fā)系統(tǒng)。如：ITL（區(qū)間時(shí)序邏輯），區(qū)段演算（DC），hoare 邏輯，WP演算，模態(tài)邏輯，時(shí)序邏輯，TAM（時(shí)序代理模型），RTTL（實(shí)時(shí)時(shí)序邏輯）等。

3）代數(shù)方法：通過(guò)將未定義狀態(tài)下不同的操作行為相聯(lián)系，給出操作的顯式定義。與基于模型的方法相同的是，沒(méi)有給出并發(fā)的顯式表示。如：OBJ， Larch族代數(shù)規(guī)約語(yǔ)言等；

4）過(guò)程代數(shù)方法：通過(guò)限制所有容許的可觀察的過(guò)程間通信來(lái)表示系統(tǒng)行為。此類(lèi)方法允許并發(fā)過(guò)程的顯式表示。如：通信順序過(guò)程（CSP），通信系統(tǒng)演算（CCS），通信過(guò)程代數(shù)（ACP），時(shí)序排序規(guī)約語(yǔ)言（LOTOS），計(jì)時(shí)CSP(TCSP），通信系統(tǒng)計(jì)時(shí)可能性演算（TPCCS）等。

5）基于網(wǎng)絡(luò)的方法：由于圖形化表示法易于理解，而且非專(zhuān)業(yè)人員能夠使用，因此是一種通用的系統(tǒng)確定表示法。該方法采用具有形式語(yǔ)義的圖形語(yǔ)言，為系統(tǒng)開(kāi)發(fā)和再工程帶來(lái)特殊的好處。如 Petri圖，計(jì)時(shí)Petri圖，狀態(tài)圖等。