基于Event-B的形式化建模關(guān)鍵技術(shù)研究

吳 勁，陳志慧

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

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

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

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

1 Event-B和Rodin平臺

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

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

圖1 Event-B模型

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

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

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

2.1 文件系統(tǒng)的初始模型

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

表1 初始模型的需求描述

2.1.1 Context的定義

首先創(chuàng)建樹型文件系統(tǒng)初始模型的靜態(tài)部分CTX01，定義集合OBJECT用于描述樹型結(jié)構(gòu)中的所有節(jié)點，定義常量root、objrel、tcl、objfn分別表示根節(jié)點、OBJECT到OBJECT的有序?qū)Φ膬缂鬟f閉包、子節(jié)點與父節(jié)點的對應(yīng)關(guān)系，它們必須滿足以下公理：

2.1.2 Machine定義

創(chuàng)建樹型文件系統(tǒng)初始模型的動態(tài)部分MCH00，引用CTX01，定義變量objects、parent，其中objects表示樹型結(jié)構(gòu)中的節(jié)點，parent表示樹型結(jié)構(gòu)中節(jié)點的父子對應(yīng)關(guān)系，定義以下不變式：

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

定義以下定理：

本文通過定理thm4對于需求Req1.4進(jìn)行規(guī)約，確保從根節(jié)點能夠到達(dá)每個節(jié)點，定理thm3用來證明thm2，定理thm4用來證明thm3。

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

2.2 第一次精化

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

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

創(chuàng)建MCH01對MCH00進(jìn)行精化，在MCH01中定義了變量files、directories，繼續(xù)使用了MCH00中的變量parent。變量files描述了樹型文件系統(tǒng)中的所有文件的集合，變量directories描述了樹型文件系統(tǒng)中的所有目錄的集合。定義了以下不變式：

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

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

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

2.3 第二次精化

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

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

2.3.1 Context的精化

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

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

2.3.2 事件的精化

創(chuàng)建machine MCH02對machine MCH01進(jìn)行精化，引用CTX02。MCH02的不變式定義如下：

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

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

2.4 第三次精化

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

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

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

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

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

3 模型驗證

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

4 結(jié) 束 語

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

[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.

編 輯 漆 蓉