B方法在軟件開發和學習中的探討

0.前言

事實證明，形式化方法在軟件開發的過程中以精確的數學語義為基礎，能精確描述系統規范， 嚴格驗證規范的性質， 從而更好地保證軟件的一致性和可靠性。其B方法的設計目的更是為了規范軟件開發的流程和可靠性，其開發的思想也值得在其他學習領域借鑒。本文在閱讀相關文獻的前提下，消化形式化方法的概念和B方法開發軟件的基本思路和方法，并參考B方法的開發思想對當前本人的研究工作進行探討。

1.形式化方法概述

形式化方法是基于數學方法來描述目標軟件系統性質的一門技術，它用嚴格的數學符號和數學法則對目標軟件系統的結構與行為進行有效地綜合、分析和推理，它為系統的說明、開發和驗證提供了一個框架，利于發現目標軟件系統需求中的不一致性、不完整性、不確定性等方面的問題。目前流行的形式化技術有：有窮狀態機、Petri網、Z語言、B方法。

1.1形式化方法在軟件開發中的作用

首先是對軟件要求的描述。軟件要求的描述是軟件開發的基礎，比如說一般非形式化的描述很可能導致描述的不明確和不一致。如果描述的不明確和不一致導致設計、編程的錯誤，將來的修改所要付出的代價就非常大。形式化方法則要求描述的明確性，而描述的不一致性也就相對易于發現。

其次是對軟件設計的描述。軟件設計的描述和軟件要求的描述一樣重要。形式化方法的優點對于軟件要求的描述同樣適用于軟件設計的描述。對于簡單的系統，形式化的描述有可能直接轉換成可執行性程序，這就簡化了軟件開發過程，節約資源和減少出錯的可能性。

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

1.2 B方法

B方法的開發從早期就是與工業界的實際應用一起進步的，在其發展過程中，人們就已經用它作為工具開發了一系列關鍵性的應用軟件系統。一個早期的重要應用是巴黎地鐵列車的信號系統，這一系統為減少剎車距離、提高整個地鐵系統得安全作出了顯著的貢獻。B發展到今天，B方法所用的符號和方法支持大部分的軟件過程：需求分析、規格說明、軟件設計、實現和維護，以及分層軟件的逐步構造的確認和驗證是B方法的指導性原則。B方法對實際大型軟件的開發起了很重要的作用。

使用B方法開發時，首先需要建模，用B的表示來描述系統變量的主要狀態、屬性及其在操作中的轉變，為系統的實現書寫規格說明，在此基礎上逐步求精，直到產生一個系統的完整實現。該方法通過一組計算機輔助工具支持規約到實現的全過程開發工作，是一種廣譜語言。B-Toolkit包含自動及交互的理論證明工具、一套軟件開發工具：AMN類型檢驗器，規約動畫，證明法則生成器，規約和代碼生成器。所有開發工具都由一個公共平臺支持：B-Tool。最后。通過模式匹配和規則重寫機制，對形式化對象生成程序。B語言中結構化的機制像其他面向對象方法一樣，增強了信息隱藏和數據封裝，嚴密的部件接口控制確保了大型開發中各個部件的獨立開發。

2.基于B方法的軟件開發過程

B方法的設計目標是作為一種實用的軟件形式化方法。作為其先驅的Z 和VDM 等方法，主要關注軟件規范說明的描述和性質證明， 沒有特別考慮支持基于它們的軟件開發過程， 也沒有考慮最終代碼的自動生成等問題。而B方法則希望支持從規范說明到代碼生成的整個軟件開發周期。使用B方法開發軟件，提倡從更抽象的描述層次開始進行開發， 先用抽象機描述軟件系統的抽象結構和抽象功能， 而后對其進行逐步精化。B方法并不嚴格區分軟件的抽象規范、設計和實現之間的差異， 軟件規范及其后續的逐層精化都統一用抽象機描述。B方法支持采用從抽象到具體的逐步構造、逐步驗證的分層開發方法進行軟件開發。

3.B方法開發思想精髓及在學習中的應用

3.1 B方法開發思想之規范和精化

規范和精化是B方法在軟件開發中的前提和重要工作，也是該方法的精髓所在。通過，不斷的規范和精化，不斷精確描述系統的需求，從一個概要的模型逐漸形成一個精確的軟件模型，一個可靠、一致、經過嚴格驗證的模型，為設計開發打下重要的基礎。

3.2規范與精化在學習設計中的啟示

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

首先是規范描述該系統。根據監控系統工作流程如下：當用戶嘗試訪問預定義好的涉密文件和系統關鍵文件時，系統自動判斷用戶權限，禁止或者允許其對文件進行操作，同時記錄用戶的行為，記錄在本地日志的同時上報服務器，使得有規范的管理和約束用戶行為，同時有效保護涉密文件和系統安全。根據流程，要對系統流程中涉及到的操作對象、操作行為以及行為和對象之間的關系描述清楚，并驗證討論其可行性。

其次是建立抽象模型。在規范的基礎上，構造系統總的框架，以及數據流向，分析功能模塊，得到基本的系統模型。此模型要滿足基本的需求。

接著是在抽象模型上精化系統。在基本的模型中，加入功能模塊的設計，并在不斷的精化過程中，把各種細節問題加進去考慮，如監控日志如何上報，如果分等級上報，用戶群權限獲取和區分、在線和離線的監控問題。不斷細化功能模塊，直至最詳細的操作過程和功能函數原型。

最后是進行程序實現。對上一個步驟的各個函數進行實現，進而實現整個系統。

4.結束語

本文通過對B方法的學習，了解了基本的形式化方法在軟件開發中的應用，以及從B方法開發思想中得到些許啟發，有助于更好地解決目前職校教學中計算機軟件開發教學方面存在的問題。

【參考文獻】

[1]陳丹敏，裘宗燕.基于B 方法的應用軟件開發.計算機與信息工程學院，2009.

[2]張志峰.B方法和構件技術在信息系統形式化開發中的應用研究.西安理工大學，2006.

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