形式化方法在軟件開(kāi)發(fā)中的應(yīng)用

摘 要：形式化方法是把概念、判斷、推理轉(zhuǎn)化成特定的形式符號(hào)后，對(duì)形式符號(hào)表達(dá)系統(tǒng)進(jìn)行研究的方法。是用具有精確語(yǔ)義的形式語(yǔ)言書(shū)寫(xiě)的程序功能描述，它是設(shè)計(jì)和編制程序的出發(fā)點(diǎn)，也是驗(yàn)證程序是否正確的依據(jù)。形式化方法就是用符號(hào)化的數(shù)學(xué)變換把需求分析給準(zhǔn)確的表述出來(lái)，這樣可以確保和需求的一致性，并能用于分析和驗(yàn)證應(yīng)用程序。

關(guān)鍵詞：形式化方法；軟件開(kāi)發(fā)

中圖分類(lèi)號(hào)：TP311.52

眾所周知，軟件開(kāi)發(fā)過(guò)程中系統(tǒng)安全是至關(guān)重要的，任何一個(gè)小的錯(cuò)誤都可能導(dǎo)致不可逆的災(zāi)難性后果，因此這就要求我們?cè)陂_(kāi)發(fā)應(yīng)用程序時(shí)設(shè)計(jì)和實(shí)現(xiàn)必須保證100%的正確，不能出現(xiàn)任何錯(cuò)誤。例如：飛行導(dǎo)航系統(tǒng)、衛(wèi)星系統(tǒng)、機(jī)器人控制等。我們?nèi)绾尾拍艽_保盡量少出現(xiàn)或者不出現(xiàn)問(wèn)題呢？大家都知道，軟件開(kāi)發(fā)必經(jīng)的幾個(gè)階段（需求分析，概要設(shè)計(jì)，詳細(xì)設(shè)計(jì)，實(shí)現(xiàn)），越在后面階段發(fā)現(xiàn)問(wèn)題，我們付出的成本和風(fēng)險(xiǎn)就會(huì)越高，我們必須在需求分析階段明確并準(zhǔn)確的描述問(wèn)題并且保證問(wèn)題描述的一致性，而且必須以設(shè)計(jì)為基礎(chǔ)對(duì)問(wèn)題加以深入的分析。這就要求我們使用符號(hào)化的方法來(lái)表述需求，即形式化描述。

1 形式化方法

1.1 形式化方法的概念

形式化方法是把概念、判斷、推理轉(zhuǎn)化成特定的形式符號(hào)后，對(duì)形式符號(hào)表達(dá)系統(tǒng)進(jìn)行研究的方法。是用具有精確語(yǔ)義的形式語(yǔ)言書(shū)寫(xiě)的程序功能描述，它是設(shè)計(jì)和編制程序的出發(fā)點(diǎn)，也是驗(yàn)證程序是否正確的依據(jù)。形式化方法就是用符號(hào)化的數(shù)學(xué)變換把需求分析給準(zhǔn)確的表述出來(lái)，這樣可以確保和需求的一致性，并能用于分析和驗(yàn)證應(yīng)用程序。畢竟，一個(gè)程序本身就是一個(gè)正式的規(guī)范化語(yǔ)言。

1.2 形式化方法的使用

形式化方法雖然能夠準(zhǔn)確、精確地規(guī)范和驗(yàn)證開(kāi)發(fā)的軟件系統(tǒng)，但是形式化方法也不是萬(wàn)能的，并不是普遍適用于所有的軟件項(xiàng)目，一些應(yīng)用程序是很好理解的，直接實(shí)現(xiàn)就好，也有一些應(yīng)用程序很小，又很好理解，應(yīng)用形式化方法就是浪費(fèi)時(shí)間。例如：簡(jiǎn)單的計(jì)算器的實(shí)現(xiàn)，電話(huà)簿的實(shí)現(xiàn)根本不需要用形式化方法。當(dāng)然也不是說(shuō)復(fù)雜的程序必須應(yīng)用形式化方法，也要視情況而定。針對(duì)一個(gè)較復(fù)雜的程序，形式化方法也可以只對(duì)一個(gè)部分進(jìn)行描述，因?yàn)椴糠挚赡苁欠治龊驮u(píng)估的關(guān)鍵。比如，圖形用戶(hù)界面設(shè)計(jì)（GUI）通常是不用形式化方法的。也可以不用的部分使用不同的形式化方法，這必須要考慮兼容性問(wèn)題和整合問(wèn)題。

2 形式化方法的選擇

針對(duì)不同的系統(tǒng)，并不是所有形式化方法都是可用的，每一種形式化方法都有不同的數(shù)學(xué)定義，通過(guò)類(lèi)型分析決定應(yīng)用程序采用何種形式化方法；一是面向?qū)ο蟮男问交椒?，通過(guò)定義狀態(tài)和操作進(jìn)行建模，比如：Z語(yǔ)言、VDM、B、Object-Z等方法。二是面向?qū)傩缘男问交椒ǎ热纾篛BJ3、Larch等方法。三是基于并發(fā)性的形式化方法，比如CCS、ACP、CSP、LOTOS等方法。四是基于實(shí)時(shí)性的形式化方法，比如TRIO、RTOZ等方法。

3 形式化方法的應(yīng)用

3.1 Z語(yǔ)言的介紹

Z語(yǔ)言產(chǎn)生于牛津大學(xué)，經(jīng)過(guò)多年的演化其語(yǔ)法和語(yǔ)義與最初版本發(fā)生了很大的變化，目前標(biāo)準(zhǔn)由國(guó)際標(biāo)準(zhǔn)化組織所統(tǒng)一，它是一種很受歡迎的語(yǔ)言，因?yàn)樗芎?jiǎn)單，它允許非正式和正式的描述混合在一起使用，并被廣泛的文獻(xiàn)和工具所支持。Z語(yǔ)言是一種基于模型的（描述狀態(tài)和操作），使用集合概念和邏輯判斷，操作表述為使用前置條件和后置條件對(duì)程序進(jìn)行定義。牛津大學(xué)曾獲得兩次Queen’s Award 展示了Z語(yǔ)言在工業(yè)上得應(yīng)用，加拿大的安大略（Ontario Hydro）是另一個(gè)展示Z語(yǔ)言在工業(yè)上的應(yīng)用。其競(jìng)爭(zhēng)對(duì)手主要為VDM-SL（Vienna Development Method-Specification Language）和B，VDM是一種廣泛應(yīng)用于工業(yè)界的形式化開(kāi)發(fā)方法，數(shù)學(xué)的精確性使它能夠有效地保證系統(tǒng)的設(shè)計(jì)和開(kāi)發(fā)。基于Z語(yǔ)言又有一些面向?qū)ο蟮臄U(kuò)展，比如：Z++、ZEST、MOOZ、Object-Z。其中Zest（The Eclipse Visualization Toolkit）是在Eclipse 平臺(tái)基礎(chǔ)上開(kāi)發(fā)的一套可視化圖形構(gòu)件集合；Object-Z語(yǔ)言產(chǎn)生于The University of Queens Land（澳大利亞），是Z語(yǔ)言的擴(kuò)展版本，其語(yǔ)義也是Z語(yǔ)言語(yǔ)義的擴(kuò)展版本，已被Software Verification Research Center （澳大利亞政府和很多企業(yè)資助的重要的研究中心）用在多個(gè)項(xiàng)目中。

3.2 形式化方法的簡(jiǎn)單應(yīng)用

我們以O(shè)bject-Z語(yǔ)言為例來(lái)說(shuō)明形式化方法的應(yīng)用，例如，一個(gè)小公司有兩個(gè)部門(mén)，每個(gè)員工屬于兩個(gè)部門(mén)中的一個(gè)部門(mén)，而且每個(gè)員工有一個(gè)工號(hào)，姓名，地址和聯(lián)系方式；（1）向部門(mén)1添加一個(gè)員工；（2）向部門(mén)2添加一個(gè)員工；（3）從部門(mén)1調(diào)到部門(mén)2一個(gè)員工以及從部門(mén)2調(diào)到部門(mén)1一個(gè)員工；（4）修改公司一個(gè)部門(mén)員工的地址；（5）報(bào)告在一個(gè)地址住得員工個(gè)數(shù)。

3.2.1 形式化描述

形式化描述是以需求和可設(shè)計(jì)為基礎(chǔ)明確并準(zhǔn)確的描述問(wèn)題并且保證問(wèn)題描述的一致性，對(duì)問(wèn)題加以深入的分析。使用基于數(shù)學(xué)邏輯的形式化方法進(jìn)行描述。首先，根據(jù)需求對(duì)公司和員工進(jìn)行建模，然后采用根據(jù)功能性需求設(shè)定模型的方法。下面是基于形式化方法的具體實(shí)現(xiàn)。

注：其中，[STRING]是基類(lèi)，然后創(chuàng)建一個(gè)Person類(lèi)，包含四個(gè)屬性（員工號(hào)、姓名、地址和聯(lián)系方式）和兩個(gè)方法（修改地址和修改聯(lián)系方式）。

注：公司類(lèi)有兩個(gè)屬性即部門(mén)1和部門(mén)2都為員工的集合，下面是約束條件，確保沒(méi)有一個(gè)人既屬于部門(mén)1又屬于部門(mén)2；隨后為初始化方法，即兩個(gè)部門(mén)都為空；然后是公司的方法（向部門(mén)1添加一個(gè)員工，向部門(mén)2添加一個(gè)員工，從部門(mén)1調(diào)到部門(mén)2一個(gè)員工，從部門(mén)2調(diào)到部門(mén)1一個(gè)員工）；然后是改變公司員工的住址的方法；最后是報(bào)告具有相同地址的人數(shù)。

3.2.2 形式化描述的實(shí)現(xiàn)

對(duì)于實(shí)現(xiàn)，由于程序較為簡(jiǎn)單，我們可以采用直接生成代碼，這樣就簡(jiǎn)化了軟件開(kāi)發(fā)的過(guò)程，并且通過(guò)一致性驗(yàn)證減少了出錯(cuò)的可能性，對(duì)此我們可以節(jié)約很多資源。采用構(gòu)造方法基于從低級(jí)規(guī)范直接導(dǎo)出程序?qū)⒊绦蚺c它的形式描述對(duì)應(yīng)起來(lái)，這樣也能把構(gòu)造與驗(yàn)證相統(tǒng)一。同時(shí)形式化方法也能自動(dòng)生成測(cè)試用例，簡(jiǎn)化了測(cè)試。

4 結(jié)束語(yǔ)

形式化方法是以簡(jiǎn)化應(yīng)用程序開(kāi)發(fā)，用簡(jiǎn)化的規(guī)范化語(yǔ)言準(zhǔn)確并精確地描述需求，并保證需求與程序的一致性，采用所支持的工具自動(dòng)或辦自動(dòng)地生成程序代碼，通過(guò)一致性驗(yàn)證保證程 序的正確性。

參考文獻(xiàn)：

[1]屈延文.形式語(yǔ)義學(xué)基礎(chǔ)與形式說(shuō)明[M].北京：科學(xué)出版社，2010.

[2]虞慧群，許浩，劉冬梅等.一種基于Object-Z的面向方面建模方法[J].華東理工大學(xué)學(xué)報(bào)（自然科學(xué)版），2008.

[3]繆淮扣，李剛，朱關(guān)銘.軟件工程語(yǔ)言-Z[M].上海：上海科學(xué)技術(shù)文獻(xiàn)出版社，1999.

[4]JIM W，PETER G L，JUAN B，et al. Formal methods：Practice and experience [J].Journal of ACM Computing Surveys，2009.

[5]李瑩，吳江琴.軟件工程形式化方法與語(yǔ)言[M].杭州：浙江大學(xué)出版社，2010.

[6]繆淮扣，陳怡海.軟件形式規(guī)格說(shuō)明語(yǔ)言-Z[M].北京：清華大學(xué)出版社，2012.

作者簡(jiǎn)介：曹斌，男，助教，研究方向：軟件工程、網(wǎng)絡(luò)、iOS研究。

作者單位：黃淮學(xué)院信息工程學(xué)院，河南駐馬店 463000