王燁凱，蘇 雯

(上海大學(xué) 計(jì)算機(jī)工程與科學(xué)學(xué)院，上海 200444)

0 引 言

混合系統(tǒng)[1]是一個(gè)日益重要的新興領(lǐng)域，它經(jīng)常出現(xiàn)在汽車工業(yè)、航空、工廠自動(dòng)化等領(lǐng)域。Event-B[2]是基于集合和一階謂詞邏輯的形式化系統(tǒng)開發(fā)方法，將混合系統(tǒng)進(jìn)行Event-B形式化建模很好地解決其復(fù)雜的系統(tǒng)設(shè)計(jì)的方法。在使用Event-B方法的建模的工具支持上，Abrial等開發(fā)了Rodin平臺(tái)為Event-B方法提供了開發(fā)建模的基礎(chǔ)平臺(tái)。許多學(xué)者為Rodin平臺(tái)擴(kuò)展了功能，如UML-B[4]工具提供了圖形化建模功能；EventB2 Java[5]工具提供了Event-B語(yǔ)言轉(zhuǎn)化成Java語(yǔ)言的工具；事件精化結(jié)構(gòu)工具[6]為事件精化結(jié)構(gòu)方法提供了工具支持；特征組合工具支持“特征”的組合和重用等等，在精化和組合的工具支持上都僅針對(duì)于特定方法進(jìn)行輔助。由于時(shí)間約束問(wèn)題的對(duì)于混合系統(tǒng)建模的重要性，文獻(xiàn)[3]對(duì)現(xiàn)有的Event-B混合系統(tǒng)建模方法進(jìn)行改進(jìn)，提出基于混合系統(tǒng)的時(shí)序約束建模方法，可以很好地刻畫混合系統(tǒng)中的時(shí)間約束問(wèn)題并支持混合系統(tǒng)時(shí)間約束的精化和組合?，F(xiàn)有的工具需手工參與多，難以輔助自動(dòng)化開發(fā)，因此需要有針對(duì)時(shí)間約束的混合系統(tǒng)模型自動(dòng)精化和組合的工具。為此我們先提出了基于混合系統(tǒng)時(shí)序模型的自動(dòng)精化和組合方法，然后開發(fā)了基于該方法的混合系統(tǒng)時(shí)序模型的自動(dòng)精化和組合的工具。工具提供了一個(gè)用戶友好的操作界面，并且擁有自動(dòng)化性能，使用戶可以用最少的操作實(shí)現(xiàn)功能。工具在保證模型正確性的前提下，能夠根據(jù)自行精化和組合方法形成的規(guī)則庫(kù)，對(duì)模型進(jìn)行快速的精化和組合。工具中的規(guī)則庫(kù)支持可重用，根據(jù)不同的建模理論可以制定不同的規(guī)則庫(kù)來(lái)適應(yīng)不同的情況。

1 背景方法介紹

本節(jié)將先介紹形式化語(yǔ)言Event-B的基本知識(shí)，然后簡(jiǎn)要介紹工具開發(fā)用到的工具平臺(tái)Rodin。

1.1 Event-B介紹

Event-B是基于一階邏輯謂詞和集合論，描述離散變遷系統(tǒng)的形式化建模方法。Event-B模型由環(huán)境(Context)和機(jī)器(Machine)組成。環(huán)境包含了模型的靜態(tài)部分，這些是描述這些常量屬性的常數(shù)(Constant)和公理(Axiom)。機(jī)器包含著模型的動(dòng)態(tài)部分，機(jī)器是由狀態(tài)(State)定義，該狀態(tài)由變量定義。變量(例如常量)對(duì)應(yīng)于簡(jiǎn)單的數(shù)學(xué)對(duì)象，例如集合、二元關(guān)系、函數(shù)、數(shù)字等，它們受不變量(Invariant)的約束。當(dāng)變量(Variable)值變化的時(shí)候，不變式性質(zhì)保持不變。除了狀態(tài)(State)之外，機(jī)器還包含許多事件(Event)，這些事件指定狀態(tài)如何演變。每個(gè)事件都由衛(wèi)兵條件(Guard)和動(dòng)作(Action)組成。衛(wèi)兵條件是事件發(fā)生的必要條件。顧名思義，動(dòng)作決定了事件發(fā)生時(shí)狀態(tài)變量的演化方式。一個(gè)事件可能含有局部的事件參數(shù)，參數(shù)可以充當(dāng)不同的功能。我們用以下3種形式指定一個(gè)名為evt的事件

evtanytwhere P(t,v) then S(t,v) end
evtwhen P(t,v) then S(v) end
evtbegin S(v) end

其中， P(t,v) 是表示衛(wèi)兵條件的謂詞，t表示事件本地的參數(shù)，而S(t,v) 表示更新某些變量的動(dòng)作。包含事件的機(jī)器的變量用v表示。第一個(gè)事件形式是最通用的形式，其中事件有一些參數(shù)t和衛(wèi)兵條件P(t,v)。 只要P(t,v) 保持一定的t， 它就可以在v表示的狀態(tài)下執(zhí)行。它對(duì)v的影響由動(dòng)作S(t,v) 指定。如果事件沒(méi)有任何參數(shù)，則使用事件的第二個(gè)形式。如果事件沒(méi)有參數(shù)且其衛(wèi)兵條件為真(True)，則使用第三種形式。

1.1.1 Event-B方法的精化

針對(duì)一個(gè)比較大型或者復(fù)雜的系統(tǒng)來(lái)建模，很難通過(guò)一次建模就考慮到所有模型中需要考慮到的細(xì)節(jié)。Event-B方法提供了逐步精化的方法，在精化的過(guò)程中一點(diǎn)點(diǎn)地添加模型中需要的細(xì)節(jié)，例如和系統(tǒng)中和外界的交互以及各種具體化的限制條件。

在Event-B，我們主要是對(duì)機(jī)器的精化和對(duì)環(huán)境的擴(kuò)展(Extends)來(lái)完成精化的工作。精化過(guò)程中我們常常需要引入新的環(huán)境的常量，或者是機(jī)器中的變量。

在精化的過(guò)程中我們需要時(shí)刻保持可行性證明義務(wù)規(guī)則，也就是要滿足事件執(zhí)行的邏輯合理。例如在場(chǎng)景A、不變量及局部約束I以及衛(wèi)兵條件G都成立的條件下，必須存在一個(gè)變量v′使得代表時(shí)間的前后謂詞BA成立

A(s,c),I(s,c,v),G(s,c,v,x)├?v′·BA(s,c,v,x,v′)

新事件的引入使系統(tǒng)需要增加相應(yīng)的新狀態(tài)的變化事件，即精化過(guò)程中還需要保證不變式依然保持證明義務(wù)

A(s,c),T(s,c),I(s,c,v),G(s,c,v),BA(s,c,v,v′)
├I(s,c,v)

1.1.2 Event-B方法的組合

Event-B方法的組合其實(shí)就是將兩個(gè)機(jī)器按照特定的方式結(jié)合在一起，結(jié)合完成后的機(jī)器必然同樣需要保持可行性證明義務(wù)規(guī)則。下面簡(jiǎn)要介紹Event-B模型組合的3種方法?；诠蚕碜兞康慕M合方法、基于共享事件的組合方法以及事件融合的組合方法。

基于共享變量的組合方法是基于共享變量的分解方法的逆方法。共享變量的分解方法會(huì)在分解時(shí)添加外部事件來(lái)模擬共享變量進(jìn)行的操作。

基于共享事件的組合方法要求被組合的事件不包含共享變量。當(dāng)系統(tǒng)可以被看作是若干個(gè)相互作用的組成部分的組合或是一個(gè)整體時(shí)，適合采用共享事件的組合方法。

事件融合組合方法同時(shí)支持上述兩種組合方法，并且其保證組合后的模型是原有模型的精化。

1.2 工具平臺(tái)介紹

Rodin平臺(tái)是Event-B語(yǔ)言的支持工具，我們的工具開發(fā)基于Rodin平臺(tái)。Rodin平臺(tái)的一個(gè)顯著特征是開放特性，它允許用戶為了更完善的方案，針對(duì)不同的任務(wù)目標(biāo)，通過(guò)其提供的接口進(jìn)行擴(kuò)展。Rodin平臺(tái)是基于Eclipse平臺(tái)并且是開源的，它的工作為嚴(yán)謹(jǐn)?shù)慕ｉ_發(fā)提供了補(bǔ)充。Rodin包含一個(gè)靜態(tài)檢查器，用于分析Event-B組件的語(yǔ)法錯(cuò)誤，包括格式正確和模型類型錯(cuò)誤。Rodin有一個(gè)證明義務(wù)發(fā)生器，用于產(chǎn)生證明義務(wù)并且這些證明義務(wù)可以由定理證明器履行。Rodin插件是提供Eclipse工作臺(tái)環(huán)境內(nèi)的特定類型的服務(wù)的組件。這里的組件既可以是在Rodin工具添加模型元素，如新的數(shù)據(jù)類型、操作等，也可以是在系統(tǒng)部署時(shí)配置到系統(tǒng)中的對(duì)象,比如模型檢查系統(tǒng)ProB[5]。我們的工具也是這么一個(gè)基于Rodin平臺(tái)的插件，可以為用戶提供較好的便利的操作。

Rodin為數(shù)據(jù)模型和鏈接插件與Event-B組件的持久層提供了API。數(shù)據(jù)模型由一系列Java接口組成，用于操縱Event-B組件的各個(gè)部分。持久層(也稱為Rodin數(shù)據(jù)庫(kù))使用XML文件存儲(chǔ)Event-B組件。Rodin使用抽象語(yǔ)法樹來(lái)存儲(chǔ)Event-B機(jī)器對(duì)變量、謂詞、集合、關(guān)系、函數(shù)，事件等的數(shù)學(xué)聲明。它還提供了遍歷樹(Walker)并將信息附加到樹的節(jié)點(diǎn)的庫(kù)。Rodin還提供了訪問(wèn)和處理證明義務(wù)的功能。我們工具的大部分實(shí)現(xiàn)是通過(guò)Java程序來(lái)實(shí)現(xiàn)的，工具通過(guò)Rodin獲取機(jī)器不變量、上下文和上下文信息、定理、公理、抽象和具體的機(jī)器變量以及一般的事件。

2 自動(dòng)化精化和組合方法

本節(jié)將先介紹文獻(xiàn)[3]提出的基于時(shí)序約束的建模理論以及其精化理論和組合理論。然后介紹根據(jù)上述精化理論和組合理論提出的自動(dòng)篩選模型方法以及自動(dòng)精化方法和自動(dòng)組合方法。

2.1 基于時(shí)序約束的建模理論

本小節(jié)介紹的理論是文獻(xiàn)[3]提出的基于時(shí)間約束的混合系統(tǒng)建模理論。在本節(jié)我們首先介紹幾個(gè)概念。

全局的時(shí)間變量now， 它用來(lái)表示當(dāng)前時(shí)間。變量now僅通過(guò)事件Click而增加，在其它時(shí)間中保持不變。

計(jì)時(shí)器變量是時(shí)序建模的重要變量。文獻(xiàn)使用count-down的設(shè)計(jì)方法來(lái)設(shè)計(jì)計(jì)時(shí)器，即將計(jì)時(shí)器設(shè)置一個(gè)初始值A(chǔ)，計(jì)時(shí)器的值會(huì)隨Click事件減少，當(dāng)計(jì)時(shí)器的值歸零的時(shí)候表示超時(shí)。不使用計(jì)時(shí)器時(shí)，可以通過(guò)普通事件將其重置。

線程集由Thread表示。線程具有自己的計(jì)時(shí)器，變量Thread用于投影以簡(jiǎn)潔地建模計(jì)時(shí)器的集合。

為了簡(jiǎn)化模型理解，下面介紹來(lái)自文獻(xiàn)[3]定義的幾個(gè)函數(shù)的含義描述。這些函數(shù)將在下文定義中用到。

setTimer(timer,b,tau) 是將計(jì)時(shí)器集合timer中b的值設(shè)置為tau。

resetUB(timer,b) 是將計(jì)時(shí)器集合timer中b的值重置為無(wú)限大。

timeOut(timer,b) 是如果線程b對(duì)應(yīng)的時(shí)間是0，那么說(shuō)明發(fā)生超時(shí)。

notTimeOut(timer,b) 是如果線程b對(duì)應(yīng)的時(shí)間大于0，那么說(shuō)明沒(méi)有超時(shí)。

decKeepZero(timer,d) 是對(duì)任何線程t∈dom(timer)， 都將timer(t) 值減少d， 若timer(t) 小于d， 則將timer(t) 記為0。

decKeepInf(timer,d) 是對(duì)任何線程t∈dom(timer)， 如果timer(t)的值是無(wú)限大，那么保持不變，否則就將其值減少d。

有3種離散的時(shí)間約束分別為延遲時(shí)間、截止時(shí)間和到期時(shí)間約束。本節(jié)中我們只把延遲時(shí)間作為例子介紹。延遲時(shí)間約束是指在前一次任務(wù)執(zhí)行后，至少再經(jīng)過(guò)時(shí)間B才執(zhí)行下一個(gè)任務(wù)。

把3種時(shí)間約束結(jié)合時(shí)鐘的概念，就可以建立對(duì)應(yīng)的時(shí)間約束模型。例如延遲時(shí)間約束的建模方式如引自文獻(xiàn)[3] 的圖1所示。根據(jù)上面解釋過(guò)的延遲時(shí)間約束的要求，我們把時(shí)間B視為執(zhí)行任務(wù)的下界約束。我們定義一個(gè)計(jì)時(shí)器變量lbTimer， 這個(gè)變量用于記錄一組下界時(shí)序約束。我們?cè)O(shè)置觸發(fā)器事件、響應(yīng)事件和Click事件。觸發(fā)器事件中定義名為setTimer的動(dòng)作將計(jì)時(shí)器lbTimer(b1) 設(shè)置成超時(shí)時(shí)間為B秒。響應(yīng)事件中定義衛(wèi)兵條件timerOut，判斷條件為lbTimer(b1)=0， 表示只有發(fā)生超時(shí)才會(huì)發(fā)生響應(yīng)事件的動(dòng)作。在Click事件中，全局時(shí)間變量now的值增加w， 下界計(jì)時(shí)器lbTimer就減少w。 但是下界計(jì)時(shí)器lbTimer不能低于0，因此如果下界計(jì)時(shí)器的值小于w， 則下一次變化不是將值減少w而是將其值直接設(shè)置為0，防止出現(xiàn)時(shí)間為負(fù)的錯(cuò)誤。其余兩種時(shí)間約束的建模方法請(qǐng)參考文獻(xiàn)[3]。

圖1 延遲模型(引用文獻(xiàn)[3])

2.2 精化理論

文獻(xiàn)[3]提出了時(shí)序模型在Event-B方法中的精化方法。文獻(xiàn)首先提出一些時(shí)鐘的基本定義。記Set(timer) 表示對(duì)事件執(zhí)行序列中的所有值進(jìn)行設(shè)置的操作。如果timer1是timer2的子序列，則意味著timer2比timer1更好。那么

Set(timer1)?Set(timer2)

(1)

設(shè)timer1和timer2為計(jì)時(shí)器，并且將timer1和timer2的最小上限定義為timer1‖timer2，其中

Set(timer1‖timer2)=Set(timer1)∪Set(timer2)

(2)

基于上述定義，給定一個(gè)抽象模型MA，該抽象模型具有一組由功能變量aTimer表示的計(jì)時(shí)器，以及一個(gè)精化模型MR，其具有一組由函數(shù)變量rTimer表示的計(jì)時(shí)器

aTimer∈aThread→R,
rTimer∈rThread→R

(3)

其中，aThread和rThread分別是模型MA和MR的線程集。

基于式(1)、式(2)，給出了計(jì)時(shí)器精化的以下定義：如果aTimer?rTimer， 則計(jì)時(shí)器rTimer可以優(yōu)化計(jì)時(shí)器aTimer， 其中aTimer?rTimer需在MR模型中證明為不變量。由以上定義展開，可以將計(jì)時(shí)器aTimer和rTimer實(shí)例化為各種計(jì)時(shí)器，以實(shí)現(xiàn)不同的目的。

Click事件的精化。如果在模型MA中把上面介紹的計(jì)時(shí)器實(shí)例化為lbTimer0、ubTimer0、exTimer0， 分別代表延遲計(jì)時(shí)器、截止計(jì)時(shí)器、到期計(jì)時(shí)器，并滿足映射條件如引自文獻(xiàn)[3]的圖2所示。那么要把模型MA精化為MR，需要滿足以下條件

圖2 Click事件精化(引用文獻(xiàn)[3])

lbTimer0?lbTimer1,ubTimer0?ubTimer1
exTimer0?exTimer1

其中，模型MR中計(jì)時(shí)器分別精化為lbTimer1、ubTimer1、exTimer1。 模型MA中的Clicka事件中的原有的計(jì)時(shí)器全部被lbTimer1、ubTimer1、exTimer1替代。上述精化過(guò)程的正確性證明過(guò)程見文獻(xiàn)[3]。

上文中介紹過(guò)3種時(shí)間約束模型，文獻(xiàn)[3]提到了對(duì)其中的延遲時(shí)間約束模型和截止時(shí)間約束模型精化的方法。

Lower Bound模型的精化。假設(shè)按照時(shí)間約束建模方式建模的LB0模型實(shí)例化的計(jì)時(shí)器名為lbTimer0。 若滿足以下條件

?t·t∈Thread?lbTimer0(t)≤lbTimer1(t)

那么計(jì)時(shí)器lbTimer0可被精化為lbTimer1。

Upper Bound模型的精化。假設(shè)按照時(shí)間約束建模方式建模的UB0模型實(shí)例化的計(jì)時(shí)器名為ubTimer0。 若滿足以下條件

?t·t∈Thread?ubTimer1(t)≤ubTimer0(t)

那么計(jì)時(shí)器ubTimer0可被精化為ubTimer1。

2.3 組合理論

文獻(xiàn)[3]同樣給出了Event-B時(shí)間約束模型的組合方法，包括計(jì)時(shí)器的組合等。我們給定模型M1和M2，分別含有計(jì)時(shí)器變量timer1和timer2滿足以下條件

timer1∈Thread→R+,timer2∈Thread→R+

當(dāng)我們把模型M1和M2組合成模型M的時(shí)候，如果模型M的組合計(jì)時(shí)器變量timer∈Thread→R+并且滿足timer=timer1∪timer2。 那么timer就成功組合了timer1和timer2, 即timer同時(shí)精化了timer1和timer2。 證明過(guò)程詳見文獻(xiàn)[3]。

Click事件的組合如引自文獻(xiàn)[3]，如圖3所示。我們以關(guān)鍵的Click事件為例，假設(shè)待組合的M1模型和M2模型中，Click事件中實(shí)例化的計(jì)時(shí)器分別為lbTimeri、ubTimeri、exTimeri(其中i=1,2)，分別代表延遲計(jì)時(shí)器、截止計(jì)時(shí)器、到期計(jì)時(shí)器。根據(jù)上面的結(jié)論可以將lbTimer1和lbTimer2組合成lbTimer， 其余兩種計(jì)時(shí)器的組合詳情見文獻(xiàn)[3]。

圖3 模型Click事件組合(引用文獻(xiàn)[3])

2.4 自動(dòng)篩選模型方法

下面我們給出篩選能應(yīng)用自動(dòng)精化理論的模型的規(guī)則，本規(guī)則針對(duì)單層模型的篩選。下述規(guī)則對(duì)于變量的要求可參考1.1節(jié)內(nèi)容。

規(guī)則1：模型滿足以下條件：

變量集合中包含計(jì)時(shí)器timer和全局時(shí)間now所實(shí)例化的變量。對(duì)于每一個(gè)計(jì)時(shí)器timer， 存在相應(yīng)的觸發(fā)-反應(yīng)事件對(duì)，它們分別是事件Trigger和事件Response的實(shí)例化。Trigger實(shí)例化事件給計(jì)時(shí)器設(shè)置超時(shí)時(shí)間，Response 實(shí)例化事件是達(dá)到觸發(fā)條件后的回應(yīng)。其中一個(gè)Trigger實(shí)例化事件或Response實(shí)例化事件可能對(duì)應(yīng)多個(gè)計(jì)時(shí)器。

單層模型的事件集合e中需包含唯一的Click事件，Click事件是完成時(shí)間自增的功能。

若符合上述條件，則認(rèn)為該模型為基于時(shí)序約束建模的基礎(chǔ)模型。

規(guī)則2：模型M1為基于時(shí)序約束建模的基礎(chǔ)模型，若模型M1使用了延遲時(shí)間約束建模方法，則模型需符合以下條件：

Response事件中包含衛(wèi)兵條件timeOut(Timer)， 且Click事件中處理計(jì)時(shí)器小于0的動(dòng)作為

decKeepZero(timer)

規(guī)則3：模型M2為基于時(shí)序約束建模的基礎(chǔ)模型，若模型M1使用了截止時(shí)間約束建模方法，則模型需符合以下條件：

Response事件中包含衛(wèi)兵條件resetUB(timer)， 在Click事件中處理計(jì)時(shí)器邊界問(wèn)題的動(dòng)作為

decKeepInf(timer)

規(guī)則4：模型M3為基于時(shí)序約束建模的基礎(chǔ)模型，若模型M1使用了到期時(shí)間約束建模方法，則模型需符合以下條件：

Response事件中包含衛(wèi)兵條件NoTimeOut(timer)， 在Click事件中處理計(jì)時(shí)器小于0的動(dòng)作為

decKeepZero(timer)

規(guī)則5：假設(shè)模型M1中含有計(jì)時(shí)器timer1， 模型M2含有計(jì)時(shí)器timer2， 且計(jì)時(shí)器timer1和timer2使用了上述規(guī)則中時(shí)間約束建模方式，那么模型M1和模型M2可以進(jìn)行基于時(shí)間約束的模型組合。

2.5 自動(dòng)精化方法

如圖4所示，抽象模型可以通過(guò)一步一步的精化成為最終的模型，精化的概念已經(jīng)在1.1.1節(jié)中介紹。下面介紹的自動(dòng)精化理論屬于在逐步精化中的一步。本文的自動(dòng)精化方法是基于文獻(xiàn)[3]提出的精化方法，面向工具層面，貼近實(shí)際操作而提出的理論。自動(dòng)精化方法需要結(jié)合2.4節(jié)的自動(dòng)篩選模型方法使用。

圖4 Event-B模型精化

(1)若模型M1被認(rèn)定為基于時(shí)序約束建模的基礎(chǔ)模型，精化方法如下：如果模型M2繼承M1，那么M2需要符合下述條件

timer0?timer1

對(duì)于?t∈dom(timer0)， 都有timer0(t)=timer1(t)， 因此模型M2的所有事件中的變量timer0都可用變量timer1表示，則此時(shí)的新模型M2就是模型M1的精化。

(2)當(dāng)模型M1中使用了延遲時(shí)間約束建模方法時(shí)，可以對(duì)模型M1進(jìn)行如下精化：如果模型M2繼承M1，那么M2需要符合下述條件

?t·t∈Thread?timer(t)≤timer1(t)

其中，Thread是所有計(jì)時(shí)器的集合。對(duì)于?t∈dom(timer)， 都有timer(t)=timer1(t)， 因此模型M2的所有事件中的變量timer0都可用變量timer1表示，則此時(shí)的新模型M2就是模型M1的精化。

(3)當(dāng)模型M1中使用了截止時(shí)間約束建模方法時(shí)，可以對(duì)模型M1進(jìn)行如下精化：如果模型M2繼承M1，那么M2需要符合下述條件

?t·t∈Thread?timer1(t)≤timer(t)

其中，Thread是所有計(jì)時(shí)器的集合。對(duì)于?t∈dom(timer)， 都有timer(t)=timer1(t)， 因此模型M2的所有事件中的變量timer0都可用變量timer1表示，則此時(shí)的新模型M2就是模型M1的精化。

2.6 自動(dòng)組合方法

Event-B模型組合，可以將兩組Event-B模型按一定的規(guī)則給合成為一個(gè)新的模型。進(jìn)行組合的兩個(gè)模型可以是精化一次也可以是精化多次。本文基于文獻(xiàn)[3]提出的組合方法，面向工具實(shí)際操作，提出了便于兩個(gè)基于時(shí)序建模的模型進(jìn)行自動(dòng)組合的理論。

若模型M1和模型M2符合2.4節(jié)中的模型組合要求，模型組合過(guò)程如圖5所示,具體組合方法如下：

圖5 Event-B模型組合

模型M3的集合、常量、公理部分繼承模型M1和M2中所有的集合、常量、公理部分。

模型M3中的變量繼承所有模型M1和M2中除計(jì)時(shí)器變量外的所有變量，并將兩個(gè)模型中的計(jì)時(shí)器變量共同精化為新變量timer。

模型M3的不變量添加條件

timer=timer1∪timer2

模型M3的不變式將根據(jù)公式追溯模型M1和M2所包含的變量，并將其屬于的類型初始化在模型M3的不變式中。

模型M3中名稱和功能相同的事件，需將兩個(gè)事件中的衛(wèi)兵條件和動(dòng)作合并繼承到同一個(gè)新事件中。

模型M3的普通事件包括初始化事件，將直接繼承模型M1和M2的普通事件。

由于新模型滿足不變式timer=timer1∪timer2， 因此將模型M3所有語(yǔ)句中的計(jì)時(shí)器timer1及timer2精化代替為timer， 并根據(jù)邏輯關(guān)系去除重復(fù)的語(yǔ)句。

3 時(shí)序約束模型的精化和組合工具

3.1 精化和組合工具概述

在本節(jié)中，我們介紹針對(duì)時(shí)序模型的自動(dòng)精化和組合工具，以幫助使用基于時(shí)序約束方法來(lái)建模的用戶更加便捷的將模型進(jìn)行精化和組合。對(duì)于Event-B的軟件工具支持常常是對(duì)某一小個(gè)功能的實(shí)踐，例如ProB這樣的模型正確性檢查工具。實(shí)際上，一個(gè)完整的建模過(guò)程不僅需要完成模型的建立，也需要對(duì)模型的語(yǔ)法語(yǔ)義以及證明義務(wù)進(jìn)行正確性的檢查等等。因此本工具建立了一個(gè)完整的工具鏈，從前期語(yǔ)法語(yǔ)義檢查到結(jié)果的正確性檢查都包含在內(nèi)。

工具鏈中包括靜態(tài)檢查器、精化/組合工具、模型檢查器3個(gè)主要組成部分，它們的鏈接方式如圖6所示。靜態(tài)檢查器主要是檢查初始抽象模型的環(huán)境和機(jī)器中是否有語(yǔ)法語(yǔ)義的錯(cuò)誤以及檢查初始抽象模型是否符合精化或組合條件的作用。通過(guò)靜態(tài)檢查器的模型會(huì)進(jìn)入精化/組合工具，精化/組合工具是根據(jù)自動(dòng)精化和組合方法形成的規(guī)則庫(kù)對(duì)模型進(jìn)行精化或組合。模型完成組合后進(jìn)入模型檢查器，模型檢查器會(huì)檢查精化和組合過(guò)后的模型的正確性。

圖6 自動(dòng)精化、組合工具鏈

本文的工具基于第2章的自動(dòng)篩選方法以及自動(dòng)精化和組合方法建立了規(guī)則庫(kù)，使得工具能夠基于既定規(guī)則為用戶提供模型的自動(dòng)精化和組合功能。規(guī)則庫(kù)的存在使得工具的可重用性大大提高，如果想要應(yīng)用其它的理論模型到本文的工具鏈，只要修改或者添加規(guī)則庫(kù)中的規(guī)則，就能又好又快地將其它理論應(yīng)用進(jìn)來(lái)。

3.2 靜態(tài)檢查器

Event-B的靜態(tài)檢查器(static checker)是用來(lái)檢查Event-B 的環(huán)境和機(jī)器中是否有語(yǔ)法的錯(cuò)誤。工具不僅結(jié)合了靜態(tài)檢查器來(lái)篩選出待精化或組合的模型中是否含有格式不正確的元素并給予反饋，還添加了一些新的功能來(lái)保證檢查結(jié)果的精度更高。

3.2.1 語(yǔ)法統(tǒng)一

語(yǔ)法統(tǒng)一的功能是為了保證后續(xù)操作的精度更高。不同的用戶在打同一句語(yǔ)句的時(shí)候，按照用戶習(xí)慣可能無(wú)意在某個(gè)地方會(huì)加入空格。空格在Event-B語(yǔ)言中不會(huì)影響一個(gè)語(yǔ)句的含義，但是不處理這個(gè)空格將會(huì)出現(xiàn)錯(cuò)誤判斷重復(fù)語(yǔ)句等問(wèn)題。因此為避免這個(gè)問(wèn)題的出現(xiàn)，工具會(huì)在整個(gè)過(guò)程中會(huì)統(tǒng)一將語(yǔ)句中的空格抹去，把句子變的緊湊、沒(méi)有空格的格式。

3.2.2 模型檢查

模型檢查的功能是為了檢查抽象模型是否符合規(guī)則庫(kù)中符合精化或組合的模型要求。在1.2節(jié)中我們介紹了Rodin平臺(tái)。在本工具中我們使用Rodin平臺(tái)提供的抽象語(yǔ)法樹來(lái)對(duì)語(yǔ)句包含的變量進(jìn)行準(zhǔn)確的切分。如若要判斷如下語(yǔ)句是否包含變量a

ab:=b+c

若不使用抽象語(yǔ)法樹，僅使用java的字符串處理函數(shù)，就會(huì)錯(cuò)誤的認(rèn)為語(yǔ)句中存在變量a。 而使用抽象語(yǔ)法樹來(lái)分析一個(gè)語(yǔ)句，其會(huì)將變量ab正確識(shí)別為一個(gè)整體，因此不會(huì)出現(xiàn)上述錯(cuò)誤。在基于抽象語(yǔ)法樹分解每一條語(yǔ)句后，我們依據(jù)規(guī)則庫(kù)中提供的接口條件，可以正確地判斷出一個(gè)模型是否符合工具繼續(xù)精化或者組合的條件。

3.3 精化和組合工具

精化和組合工具是基于上文的自動(dòng)精化和組合方法，通過(guò)Java編程的方式來(lái)實(shí)現(xiàn)規(guī)則庫(kù)中各種情況的判斷，針對(duì)性地對(duì)生成新模型，以此來(lái)進(jìn)行對(duì)抽象模型的精化或組合。精化和組合工具主要是針對(duì)模型中的機(jī)器來(lái)進(jìn)行。

3.3.1 模型生成

精化和組合都需要生成一個(gè)新模型作為精化或者組合的基礎(chǔ)模型，這樣才能進(jìn)行后續(xù)的添加刪除等操作。Rodin平臺(tái)核心庫(kù)提供了org.rodinp.core.IRodinProject包使得開發(fā)者可以方便的進(jìn)行新模型的生成、模型的繼承精化等等。工具中調(diào)用了IRodinProject包中提供的接口create，其能夠自動(dòng)生成一個(gè)新模型。然后工具再自動(dòng)的根據(jù)模型原型即需要精化或者組合的模型，把變量、不變量等內(nèi)容都繼承到新模型中。

3.3.2 精化組合規(guī)則庫(kù)

精化組合規(guī)則庫(kù)是根據(jù)自動(dòng)篩選模型方法、自動(dòng)精化方法和自動(dòng)組合方法來(lái)編寫的Java端的一個(gè)類。它的主要形式是函數(shù)，通過(guò)精化和組合工具傳遞來(lái)的不同模型信息，通過(guò)一系列按照規(guī)則制定的判斷語(yǔ)句，最后反饋給精化和組合工具需要進(jìn)行的操作結(jié)果。

3.3.3 精化工具

精化工具最主要完成的工作有兩步：第一步是添加新條件來(lái)保證精化后模型的正確性。第二步是將舊模型的變量替換成精化后的新變量。

(1)添加新條件。滿足不同的自動(dòng)精化規(guī)則對(duì)應(yīng)添加不同的條件。在完成新模型的生成之后，工具進(jìn)行一系列具體的條件判斷。例如抽象模型中含有的是下界計(jì)時(shí)器lbTimer或者是上界計(jì)時(shí)器ubTimer， 新模型中要添加的條件是不一樣的。因此工具在這部分會(huì)將模型參數(shù)輸入規(guī)則庫(kù)函數(shù)，來(lái)區(qū)分不同的情景，然后再對(duì)應(yīng)返回的結(jié)果添加不同的條件。

(2)替換變量。為了準(zhǔn)確無(wú)誤完成替換的工作，我們前期在3.2.1節(jié)已經(jīng)進(jìn)行了準(zhǔn)備工作，完成了語(yǔ)法上的統(tǒng)一，來(lái)保證替換過(guò)程中變量的識(shí)別定位準(zhǔn)確。同時(shí)我們使用了在3.2.2節(jié)用到的抽象語(yǔ)法樹，它可以保證在精化語(yǔ)句的時(shí)候不會(huì)出現(xiàn)替換上的錯(cuò)誤。

3.3.4 組合工具

首先我們可以選擇要組合的模型中其中一個(gè)模型的機(jī)器使用代碼將其精化，精化后的機(jī)器作為將要組合生成的機(jī)器的基礎(chǔ)。然后我們分3步來(lái)介紹組合的過(guò)程：

(1)組合繼承。根據(jù)自動(dòng)組合方法，組合過(guò)程中有一些參數(shù)是直接繼承到新模型中，包括集合、常量、公理等等。工具會(huì)直接將兩個(gè)的模型中的這些參數(shù)直接復(fù)制到新模型中。工具會(huì)使用Java的Hashset容器，它具有不存儲(chǔ)重復(fù)數(shù)據(jù)的特性，來(lái)輔助進(jìn)行繼承復(fù)制過(guò)程中的去除重復(fù)的工作。

為了區(qū)別兩個(gè)模型的條目，方便用戶對(duì)于模型的理解以及防止條目名稱沖突，我們會(huì)在繼承后條目名稱前面加上對(duì)應(yīng)機(jī)器的名稱，如機(jī)器Machine1的動(dòng)作act1命為Machine1.act1。

(2)組合事件。根據(jù)自動(dòng)組合方法，名稱和功能不同的事件工具會(huì)直接繼承下來(lái)。而名稱和功能相同的事件工具會(huì)將兩個(gè)事件的衛(wèi)兵條件和動(dòng)作繼承到一個(gè)事件中，同時(shí)工具將組合后事件的名稱命名為兩個(gè)機(jī)器名加上時(shí)間名的合集如Machine1.eventname ‖ Machine2.eventname。

(3)添加精化。根據(jù)自動(dòng)組合方法，我們會(huì)將兩個(gè)模型的同類計(jì)時(shí)器變量進(jìn)行精化，因此工具在識(shí)別出可精化的同類計(jì)時(shí)器后會(huì)自動(dòng)添加不變量條件以保證模型的正確性。同時(shí)工具會(huì)將模型中所有舊計(jì)時(shí)器變量替換成新計(jì)時(shí)器的名字。

3.4 模型檢查器

ProB是Rodin的一個(gè)現(xiàn)有插件。ProB支持通過(guò)模型檢查對(duì)Event-B機(jī)器進(jìn)行自動(dòng)一致性檢查，它可以用于窮盡地探索狀態(tài)空間和潛在的問(wèn)題。用戶可以在要遍歷的狀態(tài)數(shù)上設(shè)置上限，也可以在任何階段中斷檢查。當(dāng)發(fā)現(xiàn)錯(cuò)誤時(shí)，ProB將生成一個(gè)圖形來(lái)顯示錯(cuò)誤。我們的工具在模型完成精化和組合之后，結(jié)合了ProB工具對(duì)精化和組合后的模型進(jìn)行一個(gè)正確性的檢查。如果模型檢查出現(xiàn)錯(cuò)誤，將在圖形界面上反饋錯(cuò)誤的原因。

3.5 工具的界面及使用

本工具有部分輸入需要由用戶提供，為此設(shè)計(jì)了一個(gè)用戶友好的圖形界面。用戶可以在初始界面選擇進(jìn)行模型的精化或者組合，具體的模型精化和組合的界面如圖7所示。工具為了最大程度上方便用戶的操作，保證工具較高的自動(dòng)化程度，因此用戶在界面中需要手動(dòng)輸入的內(nèi)容有限。

圖7 工具用戶界面

精化工具的操作步驟如下：

(1)選擇用戶當(dāng)前工作環(huán)境中所已經(jīng)建立的某個(gè)模型文件；

(2)選擇需要進(jìn)行精化的模型后點(diǎn)擊Next按鈕進(jìn)入下一個(gè)頁(yè)面并在選擇框中自動(dòng)生成可選擇的需精化的變量。其中用戶選擇的模型機(jī)器需符合2.4節(jié)中自動(dòng)篩選方法的要求；

(3)在新頁(yè)面中選擇需要精化的變量名，例如Timer0。工具會(huì)擬生成一個(gè)默認(rèn)的精化后的變量名如Timer1，用戶可以自行更改或者選擇使用默認(rèn)的名稱；

(4)在選擇完上述要素之后點(diǎn)下Refine按鈕就能自動(dòng)生成精化后的模型。

組合工具的操作步驟如下：

(1)選擇用戶當(dāng)前工作環(huán)境中所已經(jīng)建立的某個(gè)模型文件；

(2)選擇要選擇組合的兩個(gè)模型的機(jī)器，用戶選擇的模型機(jī)器同樣需要符合自動(dòng)篩選方法的要求；

(3)點(diǎn)擊Compose按鈕，工具自動(dòng)完成組合并生成組合后的模型，并反饋成功或者出錯(cuò)的信息。

4 案例研究

本節(jié)將介紹一個(gè)具體的案例來(lái)對(duì)我們工具的使用進(jìn)行解釋。本節(jié)將先大致介紹案例的背景，然后根據(jù)時(shí)序建模理論建立初始模型，并將建立好的初始模型使用工具進(jìn)行自動(dòng)精化和組合。

4.1 案例介紹

案例的示意圖如圖8所示。案例的介紹如下：

(1)圖8中T型的裝置叫做壓力機(jī)。壓力機(jī)的初始位置在中間(Middle)。壓力機(jī)可以上下移動(dòng)，可以分別處在3個(gè)位置：上(Top)、中(Middle)、下(Bottom)；

(2)圖8中左側(cè)兩個(gè)傳送帶分別對(duì)應(yīng)壓力機(jī)的中和下兩個(gè)位置；

圖8 壓力機(jī)

(3)當(dāng)壓力機(jī)處于上位置的時(shí)候，是在鍛造金屬胚子。當(dāng)壓力機(jī)處于中位置的時(shí)候是在接收新的待鍛造金屬。當(dāng)壓力機(jī)處于下位置的時(shí)候是在將鍛造好的金屬通過(guò)傳送帶運(yùn)走；

(4)因此一個(gè)完整的鍛造流程為：壓力機(jī)從中位置得到一個(gè)待鍛造金屬；壓力機(jī)上移至上位置鍛造金屬；鍛造結(jié)束后壓力機(jī)下移到下位置，金屬球傳送走；鍛造完的金屬球運(yùn)走之后，壓力機(jī)再上移回歸至初始的中位置。

4.2 初始模型

上述的壓力機(jī)的建?？梢苑殖蒪elt和press兩部分模型。belt模型是左邊傳送帶的建模，press模型是右邊壓力機(jī)的建模。我們使用Event-B方法對(duì)belt和press進(jìn)行建模。

4.2.1 belt初始模型

首先定義模型中需要用到的常量和變量。在初始的belt1模型中我們?cè)O(shè)置了變量傳感器sensor1、 下界計(jì)時(shí)器lbTimer0、 上界計(jì)時(shí)器ubTimer0、 全局時(shí)間now。 變量傳感器sensor1是如圖左邊傳送帶belt1的感應(yīng)器。其中包含Belt事件、Loading_start事件以及Click事件。

遵循第2章的方法，由于在模型中包含下界變量lbTimer0和上界變量ubTimer0， belt1模型符合自動(dòng)篩選理論，使用了延遲時(shí)間約束和截止時(shí)間約束建模方式。

4.2.2 press初始模型

初始的press0事件中設(shè)置了bottom、middle、top， 這3個(gè)變量分別對(duì)應(yīng)上述介紹中的壓力機(jī)的3個(gè)位置；設(shè)置了變量position、work1、work2、work3，position用于表示位置，work1等3個(gè)變量為布爾值，表示對(duì)應(yīng)的工作是否在進(jìn)行。其中包含Loading_start事件、Click事件、Loading事件等事件。兩個(gè)模型中功能類似的事件具有相同的名稱，這會(huì)有利于后續(xù)模型的組合。

根據(jù)時(shí)序建模的理論，我們需要將press0進(jìn)一步精化成如圖9所示press1，然后才能符合自動(dòng)篩選理論中能進(jìn)行組合的條件。我們添加常量：由3個(gè)工作時(shí)間p1、p2、p3組成的集合，即是屬于Thread線程的集合。繼續(xù)添加下界計(jì)時(shí)器lbTimer2和上界計(jì)時(shí)器ubTimer2， 并且在主要的Loading_start事件、Loading事件和Click事件中都相應(yīng)添加了計(jì)時(shí)器的衛(wèi)兵條件和動(dòng)作。

圖9 模型press0和精化后的模型press1

4.3 工具自動(dòng)精化和組合

4.3.1 belt模型自動(dòng)精化

我們使用精化工具將belt1自動(dòng)精化為如圖10所示的belt2。可以看到，模型經(jīng)過(guò)工具的精化模塊之后，事件Belt、Loading_start、Click中的lbTimer0和ubTimer0被相應(yīng)精化成了lbTimer1和ubTimer1。 并且工具根據(jù)自動(dòng)精化方法自動(dòng)為新模型添加了新的不變量條件：

圖10 模型belt1和精化后的模型belt2

lbTimer0?lbTimer1,ubTimer0?ubTimer1

4.3.2 belt和press模型自動(dòng)組合

通過(guò)上節(jié)belt模型的自動(dòng)精化后，可以看到此時(shí)的模型belt2和press1符合工具規(guī)則庫(kù)的組合條件。通過(guò)模型驗(yàn)證后兩個(gè)模型進(jìn)入本文工具的模型組合部分可以將兩個(gè)模型進(jìn)行自動(dòng)組合。使用工具組合后的結(jié)果如圖11所示，隱去了非主要事件，重點(diǎn)展示組合相關(guān)的Loading_start事件、Click事件等。

圖11 模型press1和belt2組合后的模型

根據(jù)第2章中的自動(dòng)組合方法，我們工具逐條模擬了其中的組合方法對(duì)兩個(gè)模型進(jìn)行了組合。根據(jù)自動(dòng)組合方法，兩個(gè)模型的集合s、常量c、公理A組合后的結(jié)果是兩個(gè)模型原本條件的并集。工具在保證去除重復(fù)的前提下，將兩個(gè)模型的集合s、常量c和公理A都繼承到了組合后的模型中。接著工具針對(duì)有相同名稱和類似功能的事件按照自動(dòng)組合方法進(jìn)行了組合。例如Click事件，在衛(wèi)兵條件部分工具自動(dòng)讀取了兩個(gè)模型的Click事件的衛(wèi)兵條件部分，判斷出有一個(gè)w>0的條件重復(fù)。重復(fù)的條件僅繼承一次，剩余的條件原樣地繼承到組合后的模型中來(lái)。在動(dòng)作部分工具也進(jìn)行了類似的操作。最后組合的結(jié)果經(jīng)過(guò)工具的模型檢查模塊，顯示模型檢驗(yàn)正確。

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

本文首先介紹了基于時(shí)序約束的混合系統(tǒng)的Event-B建模方法，為了讓用戶使用此方法對(duì)混合系統(tǒng)進(jìn)行快速建模以及自動(dòng)的精化和組合，我們根據(jù)此方法提出了使用時(shí)序約束方法建模的模型的自動(dòng)精化和組合方法。我們開發(fā)了相應(yīng)的自動(dòng)精化和組合工具，結(jié)合其它的工具形成工具鏈。工具鏈中的每個(gè)模塊緊密聯(lián)系而又相互獨(dú)立，擁有可重用性和可擴(kuò)展性。

Event-B方法擁有強(qiáng)大的組件工具的支撐。我們希望在未來(lái)的工具開發(fā)中，能夠深化和其它Event-B功能組件的融合，發(fā)揮本工具的可擴(kuò)展性，設(shè)計(jì)構(gòu)想良好的用戶操作界面。我們希望開發(fā)人員可以最大程度便捷地添加其建模方法進(jìn)入本工具鏈；用戶可以簡(jiǎn)潔明了地選擇他們需要的建模方法來(lái)進(jìn)行自動(dòng)化建模。