基于時序約束建模的自動精化和組合工具

王燁凱，蘇 雯

(上海大學 計算機工程與科學學院，上海 200444)

0 引 言

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

1 背景方法介紹

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

1.1 Event-B介紹

Event-B是基于一階邏輯謂詞和集合論，描述離散變遷系統(tǒng)的形式化建模方法。Event-B模型由環(huán)境(Context)和機器(Machine)組成。環(huán)境包含了模型的靜態(tài)部分，這些是描述這些常量屬性的常數(shù)(Constant)和公理(Axiom)。機器包含著模型的動態(tài)部分，機器是由狀態(tài)(State)定義，該狀態(tài)由變量定義。變量(例如常量)對應于簡單的數(shù)學對象，例如集合、二元關系、函數(shù)、數(shù)字等，它們受不變量(Invariant)的約束。當變量(Variable)值變化的時候，不變式性質(zhì)保持不變。除了狀態(tài)(State)之外，機器還包含許多事件(Event)，這些事件指定狀態(tài)如何演變。每個事件都由衛(wèi)兵條件(Guard)和動作(Action)組成。衛(wèi)兵條件是事件發(fā)生的必要條件。顧名思義，動作決定了事件發(fā)生時狀態(tài)變量的演化方式。一個事件可能含有局部的事件參數(shù)，參數(shù)可以充當不同的功能。我們用以下3種形式指定一個名為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) 表示更新某些變量的動作。包含事件的機器的變量用v表示。第一個事件形式是最通用的形式，其中事件有一些參數(shù)t和衛(wèi)兵條件P(t,v)。 只要P(t,v) 保持一定的t， 它就可以在v表示的狀態(tài)下執(zhí)行。它對v的影響由動作S(t,v) 指定。如果事件沒有任何參數(shù)，則使用事件的第二個形式。如果事件沒有參數(shù)且其衛(wèi)兵條件為真(True)，則使用第三種形式。

1.1.1 Event-B方法的精化

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

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

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

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

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

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方法的組合其實就是將兩個機器按照特定的方式結(jié)合在一起，結(jié)合完成后的機器必然同樣需要保持可行性證明義務規(guī)則。下面簡要介紹Event-B模型組合的3種方法。基于共享變量的組合方法、基于共享事件的組合方法以及事件融合的組合方法。

基于共享變量的組合方法是基于共享變量的分解方法的逆方法。共享變量的分解方法會在分解時添加外部事件來模擬共享變量進行的操作。

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

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

1.2 工具平臺介紹

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

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

2 自動化精化和組合方法

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

2.1 基于時序約束的建模理論

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

全局的時間變量now， 它用來表示當前時間。變量now僅通過事件Click而增加，在其它時間中保持不變。

計時器變量是時序建模的重要變量。文獻使用count-down的設計方法來設計計時器，即將計時器設置一個初始值A，計時器的值會隨Click事件減少，當計時器的值歸零的時候表示超時。不使用計時器時，可以通過普通事件將其重置。

線程集由Thread表示。線程具有自己的計時器，變量Thread用于投影以簡潔地建模計時器的集合。

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

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

resetUB(timer,b) 是將計時器集合timer中b的值重置為無限大。

timeOut(timer,b) 是如果線程b對應的時間是0，那么說明發(fā)生超時。

notTimeOut(timer,b) 是如果線程b對應的時間大于0，那么說明沒有超時。

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

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

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

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

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

2.2 精化理論

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

Set(timer1)?Set(timer2)

(1)

設timer1和timer2為計時器，并且將timer1和timer2的最小上限定義為timer1‖timer2，其中

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

(2)

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

aTimer∈aThread→R,
rTimer∈rThread→R

(3)

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

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

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

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

lbTimer0?lbTimer1,ubTimer0?ubTimer1
exTimer0?exTimer1

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

上文中介紹過3種時間約束模型，文獻[3]提到了對其中的延遲時間約束模型和截止時間約束模型精化的方法。

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

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

那么計時器lbTimer0可被精化為lbTimer1。

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

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

那么計時器ubTimer0可被精化為ubTimer1。

2.3 組合理論

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

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

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

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

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

2.4 自動篩選模型方法

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

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

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

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

若符合上述條件，則認為該模型為基于時序約束建模的基礎模型。

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

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

decKeepZero(timer)

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

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

decKeepInf(timer)

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

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

decKeepZero(timer)

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

2.5 自動精化方法

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

圖4 Event-B模型精化

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

timer0?timer1

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

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

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

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

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

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

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

2.6 自動組合方法

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

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

圖5 Event-B模型組合

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

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

模型M3的不變量添加條件

timer=timer1∪timer2

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

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

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

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

3 時序約束模型的精化和組合工具

3.1 精化和組合工具概述

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

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

圖6 自動精化、組合工具鏈

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

3.2 靜態(tài)檢查器

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

3.2.1 語法統(tǒng)一

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

3.2.2 模型檢查

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

ab:=b+c

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

3.3 精化和組合工具

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

3.3.1 模型生成

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

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

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

3.3.3 精化工具

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

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

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

3.3.4 組合工具

首先我們可以選擇要組合的模型中其中一個模型的機器使用代碼將其精化，精化后的機器作為將要組合生成的機器的基礎。然后我們分3步來介紹組合的過程：

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

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

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

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

3.4 模型檢查器

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

3.5 工具的界面及使用

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

圖7 工具用戶界面

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

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

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

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

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

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

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

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

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

4 案例研究

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

4.1 案例介紹

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

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

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

圖8 壓力機

(3)當壓力機處于上位置的時候，是在鍛造金屬胚子。當壓力機處于中位置的時候是在接收新的待鍛造金屬。當壓力機處于下位置的時候是在將鍛造好的金屬通過傳送帶運走；

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

4.2 初始模型

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

4.2.1 belt初始模型

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

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

4.2.2 press初始模型

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

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

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

4.3 工具自動精化和組合

4.3.1 belt模型自動精化

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

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

lbTimer0?lbTimer1,ubTimer0?ubTimer1

4.3.2 belt和press模型自動組合

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

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

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

5 結(jié)束語

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

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