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

起源

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

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

內(nèi)容

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

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

分類

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

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

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

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

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

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

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

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

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