基于Event-B的形式化建模關鍵技術研究

吳 勁，陳志慧

(電子科技大學計算機科學與工程學院 成都 610054)

隨著全球信息化的不斷深入，軟件系統具有規模大且復雜度高的特點，而自然語言描述的軟件需求具有不確定性、二義性且缺乏對軟件需求進行嚴格檢查的有效途徑，因此無法確保軟件需求的正確性、完善性和合理性。軟件工程的實踐表明，在開發過程中，錯誤發現得越早，修復得越早，付出的代價越小。為了確保軟件的質量，在軟件開發的早期需求分析階段，采用形式化方法描述軟件的需求，并驗證模型的正確性，是確保軟件質量的有效方法。

國內外眾多學者研究如何有效地將形式化方法應用于實際的軟件開發過程，在歐美國家已有將形式化方法應用到實際項目的成功案例。如法國采用B形式化方法開發了高速鐵路控制系統，獲得成功[1]。而Event-B方法是B方法[2]的簡化，并吸取了其他的形式化方法的優點，包括Action Systems[3]、TLA+[4]、UNITY[5]等，適合開發安全性要求較高的大規模高復雜度軟件系統。

本文以文件系統建模為例，基于Rodin平臺采用Event-B語言，以逐步精化的方式向模型中添加屬性和功能達到豐富、完善、細化模型的目的，并驗證模型的正確性。

1 Event-B和Rodin平臺

Event-B是一種用于進行系統級建模和分析的形式化方法[6]，它基于集合理論，在不同的抽象級構建系統，并逐步精細化，使用數學證明來保證不同精化級別之間的一致性。Rodin是一種用于開發復雜高可信軟件系統的開放工具平臺，它基于Event-B形式化方法，提供對精化和數學證明的自然支持。

Event-B軟件系統模型如圖1所示，包含兩部分：靜態屬性和行為屬性，分別用Context和Machine進行描述。Context由集合、常量、公理和定理組成，公理用于描述集合和常量之間的關系，Context可以被繼承，也可以被Machine引用。Machine由狀態、不變式、事件和定理組成，其中狀態是用變量進行定義的在模型中必須保證無論變量的值如何改變，不變式都成立，這一性質必須以證明義務的方式進行證明[7]。一個Machine可以包含多個原子事件，原子事件代表模型發生改變的方式。

圖1 Event-B模型

建模的過程就是一個逐步精化的過程，精化方式有兩種：精化Machine的狀態和精化Machine的事件，兩種方式可同時使用。通常采用多個具體事件精化一個抽象事件，把多個抽象事件合并成一個抽象事件或引入新事件的方式來對Machine的事件進行精化。通過模型驗證來確保軟件需求模型的正確性，Rodin平臺為Event-B模型驗證提供了支持。

2 基于Event-B的形式化建模

本文基于Rodin平臺采用Event-B語言對文件系統進行建模，首先建立文件系統的樹型抽象模型，然后采用逐步精化的方式向模型中添加更多的設計細節，達到擴大模型的目的，并證明其正確性。

2.1 文件系統的初始模型

首先建立文件系統的初始模型，在這個抽象級別中將建立一個樹型文件系統的初始模型，其需求描述如表1所示(Req代表需求)。

表1 初始模型的需求描述

2.1.1 Context的定義

首先創建樹型文件系統初始模型的靜態部分CTX01，定義集合OBJECT用于描述樹型結構中的所有節點，定義常量root、objrel、tcl、objfn分別表示根節點、OBJECT到OBJECT的有序對的冪集、傳遞閉包、子節點與父節點的對應關系，它們必須滿足以下公理：

2.1.2 Machine定義

創建樹型文件系統初始模型的動態部分MCH00，引用CTX01，定義變量objects、parent，其中objects表示樹型結構中的節點，parent表示樹型結構中節點的父子對應關系，定義以下不變式：

inv1表示objects是OBJECT的子集。inv6表示根節點是objects的一個元素，在這個抽象模型中，初始化事件將objects初始化為只包含root的集合，parent初始化為空集，規約了需求Req1.1。inv8表示parents是一個全函數，這個全函數定義了除根節點外的子節點到父節點的映射，實際表示除根節點外任何節點都有一個父節點，規約了需求Req1.2。inv10規約需求Req1.3，確保在樹型文件系統中沒有環，這個不變式的定義方式由文獻[2]提出，parent～[s]得到的是集合s的直接子節點，如果síparent～[s]且s不為空，則表示parent關系中存在環，因此這個不變式表示s為空集，即parent關系中沒有環。

定義以下定理：

本文通過定理thm4對于需求Req1.4進行規約，確保從根節點能夠到達每個節點，定理thm3用來證明thm2，定理thm4用來證明thm3。

在MCH00中，定義了5個抽象事件：創建(newobj)、刪除(delete)、刪除子樹(deltree)、復制(copy)和移動(move)，其中事件copy和move操作類似，以copy為例說明事件的定義和規約方法，其定義如下：

2.2 第一次精化

本節對初始模型進行第一次精化，對初始模型中的節點進行了區別，引入了文件和目錄，第一次精化模型的需求描述如表2所示。

表2 第一次精化模型的需求描述

創建MCH01對MCH00進行精化，在MCH01中定義了變量files、directories，繼續使用了MCH00中的變量parent。變量files描述了樹型文件系統中的所有文件的集合，變量directories描述了樹型文件系統中的所有目錄的集合。定義了以下不變式：

不變式inv2定義了變量files的數據類型，表示files是objects的子集，描述的是樹型文件系統中的文件。不變式inv3定義了變量directories的數據類型，表示directories是objects的子集，描述的是樹型文件系統中的目錄。不變式inv4表示files和directories沒有交集，即不存在即是文件又是目錄的節點，inv5表示文件系統中只有文件和目錄這兩種實體，inv4和inv5共同規約了Req2.1。不變式inv6表示root是一個目錄，即規約了Req2.2。不變式inv1表示在parent關系中的父節點都是目錄類型，即規約了Req2.3。

在初始化事件中，files初始化為空集表示，沒有任何文件存在，directories初始化為只含有根目錄root，因為初始化情況下只有一個root目錄，所以也就不存在相關的parent關系，即parent等于f。在machine MCH01中，不變式inv5使用了machine MCH00中的變量objects，所以inv5是一個聯接不變式，且在inv5將抽象變量objects定義為files∪directories，所以machine MCH01中的所有objects都可以用進行替代。

在此次的事件精化的步驟是：事件mkdir和crt_file共同精化抽象事件newobj；事件move精化抽象事件move；事件delfile和rmdir共同精化抽象事件delete；事件copy精化抽象事件copy；事件deltree精化抽象事件deltree。

2.3 第二次精化

在本次精化階段，為模型引入了文件內容，文件緩沖區和意外掉電處理，根據前面的描述，第二次精化模型的需求描述如表3所示。

表3 第二次精化模型的需求描述

2.3.1 Context的精化

創建繼承CTX01的CTX02，增加3個集合DATA、NAME、DATE，其中DATA表示數據塊，NAME表示名字，DATE表示時間。它們必須滿足以下公理：

CONTENT表示文件內容，axm1說明是CONTENT是從N映射到DATA的部分函數；axm2表示文件的內容可以為空；axm7表示文件內容的長度是有限的。

2.3.2 事件的精化

創建machine MCH02對machine MCH01進行精化，引用CTX02。MCH02的不變式定義如下：

不變式inv1表示fcontent是一個從filles映射到CONTENT的全函數，規約了需求Req3.1。inv2、inv3、inv4規約了需求Req3.2。inv5、inv6規約了需求Req3.3。inv7、inv8規約了需求Req3.4。

在此次精化過程中，添加了新事件w_open、w ritefile、r_open、readfile、close、power_loss、power_on。對事件mkdir、crt_file、move、delfile、rmdir、copy、deltree分別精化相應的抽象事件。

2.4 第三次精化

本次精化的目標就是把名字、創建時間、修改時間以及文件大小這4個屬性引入模型中。第三次精化模型的需求描述如表4所示。

表4 第三次精化模型的需求描述

創建MCH03，對MCH02進行精化。在MCH03中，增加了4個變量，其中變量oname表示文件或目錄的名字，變量dateCreated表示文件或目錄的創建時間，變量dateLastModified表示文件或目錄的最后修改時間，變量file_size表示文件的大小。定義了以下不變式：

不變式inv1規約了需求Req4.1，inv2規約了需求Req4.2，inv3規約了需求Req4.3，inv4規約了需求Req4.4。

在此次精化過程中，增加了新事件rename，對MCH02中的相應事件mkdir、crt_file、move、delfile、rmdir、copy、deltree、w ritefile分別進行了精化。

3 模型驗證

通過3次精化文件系統的模型已經建立，然而工作并沒有結束，用形式化方法建立的模型要經過嚴格地數學驗證才可以確保模型的正確性，即模型生成的所有證明義務都得以證明才表示建立的模型是正確的。Rodin平臺不但為建立模型提供了開發環境而且為模型的驗證提供了支持，Rodin為開發者提供了一套自動化模型驗證工具，簡化了復雜且繁瑣的驗證過程。本文建立的樹型文件系統模型生成的所有證明義務都得以證明，證明結果如圖2所示。

4 結 束 語

軟件系統的規模和復雜程度不斷提高而傳統的需求分析方法難以確保軟件的正確性和一致性，為軟件系統的質量埋下了隱患。本文以文件系統建模為例，在軟件開發的早期需求分析階段，采用Event-B形式化方法描述軟件的需求，采用逐步精化的方式建立并驗證模型，確保了軟件的正確性，對復雜軟件系統的開發具有較好的借鑒作用。

[1] ABRIAL J R. Formal methods: Theory becoming practice[J].Journal of Universal Computer Science, 2007, 13(5):619-628.

[2] ABRIAL J R. The B-book: Assigning programs to meanings[M]. Cambridge: Cambridge University Press,1996.

[3] BACK R J, KURKI-SUONIO R. Distributed cooperation w ith action systems[J]. ACM Transaction on Programming Languages and Systems, 1988, 10(4): 513-554.

[4] LAMPORT L. Specifying systems: the TLA+ language and tools for hardware and software engineers[M]. Boston:Addison-Wesley, 1999.

[5] CHANDY K M, M ISRA J. Parallel program design, a foundation[M]. Boston: Addison-Wesley, 1988.

[6] ABRIAL J R. Modelling in Event-B: System and software engineering[M]. Cambridge: Cambridge University Press,2010.

[7] HALLERSTEDE S. On the purpose of Event-B proof obligations[J]. Formal Aspects of Computing, 2011, 23(1):133-150.

編 輯 漆 蓉