0.前言

事實(shí)證明，形式化方法在軟件開(kāi)發(fā)的過(guò)程中以精確的數(shù)學(xué)語(yǔ)義為基礎(chǔ)，能精確描述系統(tǒng)規(guī)范， 嚴(yán)格驗(yàn)證規(guī)范的性質(zhì)， 從而更好地保證軟件的一致性和可靠性。其B方法的設(shè)計(jì)目的更是為了規(guī)范軟件開(kāi)發(fā)的流程和可靠性，其開(kāi)發(fā)的思想也值得在其他學(xué)習(xí)領(lǐng)域借鑒。本文在閱讀相關(guān)文獻(xiàn)的前提下，消化形式化方法的概念和B方法開(kāi)發(fā)軟件的基本思路和方法，并參考B方法的開(kāi)發(fā)思想對(duì)當(dāng)前本人的研究工作進(jìn)行探討。

1.形式化方法概述

形式化方法是基于數(shù)學(xué)方法來(lái)描述目標(biāo)軟件系統(tǒng)性質(zhì)的一門技術(shù)，它用嚴(yán)格的數(shù)學(xué)符號(hào)和數(shù)學(xué)法則對(duì)目標(biāo)軟件系統(tǒng)的結(jié)構(gòu)與行為進(jìn)行有效地綜合、分析和推理，它為系統(tǒng)的說(shuō)明、開(kāi)發(fā)和驗(yàn)證提供了一個(gè)框架，利于發(fā)現(xiàn)目標(biāo)軟件系統(tǒng)需求中的不一致性、不完整性、不確定性等方面的問(wèn)題。目前流行的形式化技術(shù)有：有窮狀態(tài)機(jī)、Petri網(wǎng)、Z語(yǔ)言、B方法。

1.1形式化方法在軟件開(kāi)發(fā)中的作用

首先是對(duì)軟件要求的描述。軟件要求的描述是軟件開(kāi)發(fā)的基礎(chǔ)，比如說(shuō)一般非形式化的描述很可能導(dǎo)致描述的不明確和不一致。如果描述的不明確和不一致導(dǎo)致設(shè)計(jì)、編程的錯(cuò)誤，將來(lái)的修改所要付出的代價(jià)就非常大。形式化方法則要求描述的明確性，而描述的不一致性也就相對(duì)易于發(fā)現(xiàn)。

其次是對(duì)軟件設(shè)計(jì)的描述。軟件設(shè)計(jì)的描述和軟件要求的描述一樣重要。形式化方法的優(yōu)點(diǎn)對(duì)于軟件要求的描述同樣適用于軟件設(shè)計(jì)的描述。對(duì)于簡(jiǎn)單的系統(tǒng)，形式化的描述有可能直接轉(zhuǎn)換成可執(zhí)行性程序，這就簡(jiǎn)化了軟件開(kāi)發(fā)過(guò)程，節(jié)約資源和減少出錯(cuò)的可能性。

另外，形式化方法可以用于程序的驗(yàn)證，以保證程序的正確性。

1.2 B方法

B方法的開(kāi)發(fā)從早期就是與工業(yè)界的實(shí)際應(yīng)用一起進(jìn)步的，在其發(fā)展過(guò)程中，人們就已經(jīng)用它作為工具開(kāi)發(fā)了一系列關(guān)鍵性的應(yīng)用軟件系統(tǒng)。一個(gè)早期的重要應(yīng)用是巴黎地鐵列車的信號(hào)系統(tǒng)，這一系統(tǒng)為減少剎車距離、提高整個(gè)地鐵系統(tǒng)得安全作出了顯著的貢獻(xiàn)。B發(fā)展到今天，B方法所用的符號(hào)和方法支持大部分的軟件過(guò)程：需求分析、規(guī)格說(shuō)明、軟件設(shè)計(jì)、實(shí)現(xiàn)和維護(hù)，以及分層軟件的逐步構(gòu)造的確認(rèn)和驗(yàn)證是B方法的指導(dǎo)性原則。B方法對(duì)實(shí)際大型軟件的開(kāi)發(fā)起了很重要的作用。

使用B方法開(kāi)發(fā)時(shí)，首先需要建模，用B的表示來(lái)描述系統(tǒng)變量的主要狀態(tài)、屬性及其在操作中的轉(zhuǎn)變，為系統(tǒng)的實(shí)現(xiàn)書(shū)寫(xiě)規(guī)格說(shuō)明，在此基礎(chǔ)上逐步求精，直到產(chǎn)生一個(gè)系統(tǒng)的完整實(shí)現(xiàn)。該方法通過(guò)一組計(jì)算機(jī)輔助工具支持規(guī)約到實(shí)現(xiàn)的全過(guò)程開(kāi)發(fā)工作，是一種廣譜語(yǔ)言。B-Toolkit包含自動(dòng)及交互的理論證明工具、一套軟件開(kāi)發(fā)工具：AMN類型檢驗(yàn)器，規(guī)約動(dòng)畫(huà)，證明法則生成器，規(guī)約和代碼生成器。所有開(kāi)發(fā)工具都由一個(gè)公共平臺(tái)支持：B-Tool。最后。通過(guò)模式匹配和規(guī)則重寫(xiě)機(jī)制，對(duì)形式化對(duì)象生成程序。B語(yǔ)言中結(jié)構(gòu)化的機(jī)制像其他面向?qū)ο蠓椒ㄒ粯樱鰪?qiáng)了信息隱藏和數(shù)據(jù)封裝，嚴(yán)密的部件接口控制確保了大型開(kāi)發(fā)中各個(gè)部件的獨(dú)立開(kāi)發(fā)。

2.基于B方法的軟件開(kāi)發(fā)過(guò)程

B方法的設(shè)計(jì)目標(biāo)是作為一種實(shí)用的軟件形式化方法。作為其先驅(qū)的Z 和VDM 等方法，主要關(guān)注軟件規(guī)范說(shuō)明的描述和性質(zhì)證明， 沒(méi)有特別考慮支持基于它們的軟件開(kāi)發(fā)過(guò)程， 也沒(méi)有考慮最終代碼的自動(dòng)生成等問(wèn)題。而B(niǎo)方法則希望支持從規(guī)范說(shuō)明到代碼生成的整個(gè)軟件開(kāi)發(fā)周期。使用B方法開(kāi)發(fā)軟件，提倡從更抽象的描述層次開(kāi)始進(jìn)行開(kāi)發(fā)， 先用抽象機(jī)描述軟件系統(tǒng)的抽象結(jié)構(gòu)和抽象功能， 而后對(duì)其進(jìn)行逐步精化。B方法并不嚴(yán)格區(qū)分軟件的抽象規(guī)范、設(shè)計(jì)和實(shí)現(xiàn)之間的差異， 軟件規(guī)范及其后續(xù)的逐層精化都統(tǒng)一用抽象機(jī)描述。B方法支持采用從抽象到具體的逐步構(gòu)造、逐步驗(yàn)證的分層開(kāi)發(fā)方法進(jìn)行軟件開(kāi)發(fā)。

3.B方法開(kāi)發(fā)思想精髓及在學(xué)習(xí)中的應(yīng)用

3.1 B方法開(kāi)發(fā)思想之規(guī)范和精化

規(guī)范和精化是B方法在軟件開(kāi)發(fā)中的前提和重要工作，也是該方法的精髓所在。通過(guò)，不斷的規(guī)范和精化，不斷精確描述系統(tǒng)的需求，從一個(gè)概要的模型逐漸形成一個(gè)精確的軟件模型，一個(gè)可靠、一致、經(jīng)過(guò)嚴(yán)格驗(yàn)證的模型，為設(shè)計(jì)開(kāi)發(fā)打下重要的基礎(chǔ)。

3.2規(guī)范與精化在學(xué)習(xí)設(shè)計(jì)中的啟示

從上面描述可知，B方法的開(kāi)發(fā)思路適用于大多數(shù)的軟件系統(tǒng)開(kāi)發(fā)設(shè)計(jì)，即使B方法的具體技術(shù)不大適用，但是其開(kāi)發(fā)思想中的規(guī)范和精化肯定有借鑒可可取之處。以本人接下來(lái)的研究工作涉密終端基本安全基線的監(jiān)控方案的研究為例，要設(shè)計(jì)一個(gè)符合涉密終端安全需求的基本安全基線的監(jiān)控管理系統(tǒng)。在這里僅是參考B方法的開(kāi)發(fā)思想進(jìn)行設(shè)計(jì)，由于對(duì)B方法的細(xì)節(jié)并沒(méi)有掌握，因此沒(méi)法用B方法對(duì)系統(tǒng)規(guī)范和精化。

首先是規(guī)范描述該系統(tǒng)。根據(jù)監(jiān)控系統(tǒng)工作流程如下：當(dāng)用戶嘗試訪問(wèn)預(yù)定義好的涉密文件和系統(tǒng)關(guān)鍵文件時(shí)，系統(tǒng)自動(dòng)判斷用戶權(quán)限，禁止或者允許其對(duì)文件進(jìn)行操作，同時(shí)記錄用戶的行為，記錄在本地日志的同時(shí)上報(bào)服務(wù)器，使得有規(guī)范的管理和約束用戶行為，同時(shí)有效保護(hù)涉密文件和系統(tǒng)安全。根據(jù)流程，要對(duì)系統(tǒng)流程中涉及到的操作對(duì)象、操作行為以及行為和對(duì)象之間的關(guān)系描述清楚，并驗(yàn)證討論其可行性。

其次是建立抽象模型。在規(guī)范的基礎(chǔ)上，構(gòu)造系統(tǒng)總的框架，以及數(shù)據(jù)流向，分析功能模塊，得到基本的系統(tǒng)模型。此模型要滿足基本的需求。

接著是在抽象模型上精化系統(tǒng)。在基本的模型中，加入功能模塊的設(shè)計(jì)，并在不斷的精化過(guò)程中，把各種細(xì)節(jié)問(wèn)題加進(jìn)去考慮，如監(jiān)控日志如何上報(bào)，如果分等級(jí)上報(bào)，用戶群權(quán)限獲取和區(qū)分、在線和離線的監(jiān)控問(wèn)題。不斷細(xì)化功能模塊，直至最詳細(xì)的操作過(guò)程和功能函數(shù)原型。

最后是進(jìn)行程序?qū)崿F(xiàn)。對(duì)上一個(gè)步驟的各個(gè)函數(shù)進(jìn)行實(shí)現(xiàn)，進(jìn)而實(shí)現(xiàn)整個(gè)系統(tǒng)。

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

本文通過(guò)對(duì)B方法的學(xué)習(xí)，了解了基本的形式化方法在軟件開(kāi)發(fā)中的應(yīng)用，以及從B方法開(kāi)發(fā)思想中得到些許啟發(fā)，有助于更好地解決目前職校教學(xué)中計(jì)算機(jī)軟件開(kāi)發(fā)教學(xué)方面存在的問(wèn)題。

【參考文獻(xiàn)】

[1]陳丹敏，裘宗燕.基于B 方法的應(yīng)用軟件開(kāi)發(fā).計(jì)算機(jī)與信息工程學(xué)院，2009.

[2]張志峰.B方法和構(gòu)件技術(shù)在信息系統(tǒng)形式化開(kāi)發(fā)中的應(yīng)用研究.西安理工大學(xué)，2006.

[3][美]Jean-Raymond Abrial，J.-R.Abrial，裘宗燕[譯].B方法.電子工業(yè)出版社，2004.