模型精化過程中模型間一致性檢測研究

王 玲 徐立華

(華東師范大學計算機科學技術系 上海 200241)

?

模型精化過程中模型間一致性檢測研究

王 玲 徐立華

(華東師范大學計算機科學技術系 上海 200241)

傳統的模型精化過程中模型間一致性檢測專注于檢測模型自身的正確性、死鎖、以及不變式保持性等，而無法保證模型間行為方面的一致性。為此提出利用系統行為屬性來反應模型行為，結合模型檢測的方法來檢測模型間的行為一致性。首先對精化前模型分析生成抽象測試用例并抽取其代表的系統行為屬性；然后根據精化后的模型抽取模型精化關系并進一步更新系統屬性；最后使用這些系統行為屬性來驗證精化后的模型是否依然滿足其代表的系統行為，如果不滿足則說明模型間存在不一致行為，可以通過生成的反例路徑找出不一致的位置。實驗結果表明使用該方法可以有效找出模型精化前后的大多數不一致行為。

模型精化 模型檢測 一致性檢測 屬性抽取 線性時序邏輯

0 引 言

模型精化[1-4]是軟件工程中基于模型驅動開發[5-8]的關鍵問題，被廣泛應用于基于模型的驅動開發方法中。若在初始模型中引入過多細節會使得開發和測試不易管理，因此對于那些大型復雜系統的建模很難能夠做到一步到位，在實際的開發建模過程中往往采用模型精化的技術，即在原模型的基礎上添加更多的細節，逐步細化，模型從剛開始的比較抽象變得逐漸具體化。而模型精化過程中模型間的一致性是正確建模的必要前提，為了保證精化后的模型和精化前是一致的，需要對精化前后的模型進行一致性檢驗。

傳統的模型精化過程中模型間一致性檢測除了檢測模型自身的語法、語義、結構方面的正確性之外，還提供了死鎖檢測和不變式保持性檢測[30]。所謂死鎖即一個系統或系統的一部分不能再發生任何的狀態變遷，系統到達死鎖狀態后若無外力干預無法繼續執行。所謂不變式保持性即在抽象模型中已經被證明的性質，在其精化后的模型中這些性質仍然要保持不變，并且在后繼的精化模型中也要保持不變。通常而言，系統不變式定義的是系統中比較重要的或有關安全性的性質[29]，然而系統模型間的不一致往往存在于系統行為的各個方面，使用傳統的不一致檢測方法很難一一找出這些不一致。為此本文提出利用系統屬性來刻畫系統行為狀態的改變，定義為系統行為屬性，結合模型檢測的方法來檢測模型間的行為一致性。由于模型具有抽象性，模型間一致性檢測的一個難點在于如何描述出各層模型間抽象到具體的系統行為；另一難點在于如何進一步抽取出這些系統行為屬性以便下一步的模型一致性驗證。另外，由于模型的復雜性和建模者的行為習慣，導致模型精化過程中精化關系錯綜復雜，如何從這些錯綜復雜的精化關系中找出精化前后模型間的內在關聯，使得從精化前的模型中抽取的系統行為屬性能夠在精化后的模型中得到有效對應也是一個重點問題，這些問題導致模型間自動化一致性檢測成為難中之難。

為了解決上述問題，1) 使用系統行為屬性來描述各層模型間抽象到具體的關系，系統行為屬性表示為某個操作的前后置條件，通過對比前后置條件的改變可發現模型發生了哪些操作，以此來實現模型抽象到具體化描述的轉化；2) 通過動態模擬系統模型的具體執行來反映出系統行為狀態的改變，以抽象測試用例的形式記錄，將涉及的觸發事件及其相關的狀態變遷以線性時序邏輯(LTL)的形式描述，視為精化后模型需要滿足的系統行為約束，即系統行為屬性；3) 從精化后模型中的詳細信息中找出精化前后模型間的內在關系，并相應更新系統行為屬性，使得自動化一致性檢測成為可能。我們在之前的工作ProMiner[34]生成的抽象測試用例的基礎上，首先把抽象模型的系統屬性轉化為具體的系統行為屬性，實現了系統行為屬性的自動化抽取，并根據從精化后模型中抽取出的精化關系進一步更新這些系統行為屬性，最后使用這些系統行為屬性來驗證精化后的模型是否依然滿足，如果不滿足則說明模型間存在不一致行為，可以通過生成的反例路徑找出不一致的位置。實驗結果表明使用此方法可以有效找出模型精化前后的大多數不一致行為。

1 背景介紹

1.1 模型檢測

模型檢測是一種基于模型的形式化方法。模型檢測[9-12]是一種很重要的自動驗證技術，主要通過顯式狀態搜索和隱式不動點計算來驗證有窮狀態并發系統的命題性質，由于模型檢測可以自動執行，并能在系統不滿足性質時提供反例路徑，因此在工業界比演繹證明更受推崇。時態邏輯模型檢測是常用的模型檢測技術，它又可以分為基于計算樹邏輯(CTL)[13,14]的模型檢測和基于線性時序邏輯(LTL)[15]的模型檢測。其中LTL的優點主要有：易于組合驗證、性質描述和反例路徑生成更加直觀、容易實現抽象技術等，所以得到了更廣泛的關注。

使用模型檢測的方法來驗證一致性得到了廣泛的關注和認可，主要應用在硬件設計的驗證、通信協議、安全協議、控制系統、和一些軟件系統中[12]。但是大多數的模型檢測工具存在一定的局限性[9]，例如只檢測模型自身的語法、語義、結構方面的正確性和死鎖、不變式保持性等，可以找出一些很明顯的不一致，而無法找出模型中潛在的反映系統行為方面的不一致(例如兩個模型中同一操作產生了不同的結果)。模型中這些反映系統行為方面的不一致需要使用系統行為屬性來檢測驗證，而對于模型行為方面的一致性檢測較少見之于文獻。

1.2 Event-B模型

Event-B[25-27,31]是一種建模語言，運行于Rodin[28,29]上，使用Event-B語言建模的模型的核心就是基于狀態遷移系統的抽象自動機，它包含了自動機(Machine)、場景(Context)、證明義務(Proof Obligations)等。該模型可抽象表示為：Machine:=，也可以包括一些描述系統性質的不變式(invariants)。其中State為一組代表系統狀態的變量(Variable)對一個值空間的滿射，形如：State:= {var1=value1;var2=value2;var3=value3…}，其中var為變量名，value為變量取值。Event事件為一組代表系統狀態遷移的遷移，形如：Event:=any(var)where(condition)then(action)end，即對參數集var在前置條件集condition下可執行action。另外，每個Event-B模型都需要一個初始化事件(INITIALIZATION)用來指定模型的初始狀態。

ProB[30]是一個很常用的模型檢測工具，可集成在Rodin上，可使用LTL作為輸入進行驗證。ProB支持模型的自動一致性檢測，具體主要包括死鎖和不變式違反的檢測，而ProB無法檢測模型間那些潛在的反映系統行為方面屬性的一致性，所以提出使用系統行為屬性的方法來達到模型間行為方面的一致性檢測的目的，通過抽取系統行為屬性并用LTL的形式表示出來，可直接用于檢測模型間行為一致性。

1.3 一致性檢測

目前模型一致性檢測主要包括：模型與模型間、 模型與代碼間、模型內部間。其中模型與模型間的一致性是指兩個模型的基本特征是一樣的，反映的是同一個系統需求和相同的實現機制。目前模型與模型間的一致性檢測主要使用不變式保持性方法，在模型A中成立的性質，在另一個模型B中這個性質仍然要保持不變。通常系統不變式定義為系統中比較重要或有關安全性的性質，但是不變式保持性方法很難檢測到那些沒有定義為系統不變式的那些不一致，而模型精化過程中模型間一致性檢測方法通過抽取整個系統的系統行為屬性進行一致性檢測，不僅包含了對這些系統不變式的檢測而且還包含了系統中沒有定義為系統不變式的那部分不一致。一致性檢測最簡單直接的方法就是人工法，這種方法可以應用于任何模型或代碼，但對于大型復雜系統來說，使用人工法工作量巨大，容易產生人為的錯誤，自動化一致性檢測是勢在必行。目前常用的方法是通過形式化方法[35]將模型轉換為一些形式化的表示中，相對容易進行一致性檢測，但由于模型本身的抽象和復雜性，這種方法有可能執行效率不高，和工具集成起來比較困難。

1.4 屬性抽取

系統屬性抽取一直是個熱點問題。一般是直接或間接地從系統中抽取某種類型的屬性來對系統進行分析和驗證。屬性抽取是將不同信息源對于某個系統或事物的屬性集中起來，能從不同的角度反映這個系統或事物的相關情況。屬性抽取的方法可以分為基于規則的抽取和基于統計的抽取，其中基于規則的方法一般通過人工定義抽取的規則和模式進行模式匹配，基于統計的方法是一種使用機器學習算法自動抽取的技術。屬性抽取方面的工具也有很多，例如微軟實驗室的可能不變式(likely invariants)抽取工具Daikon[16-19]使用動態執行和監控變量的手段來提取系統不變式，可用來作系統分析，但Daikon是基于代碼級別的并不針對模型層面，所以不能用來做模型間的一致性檢測，模型精化過程中模型間一致性檢測方法旨在抽取系統行為屬性用于模型與模型之間的一致性檢測。Synoptic[20-24]是基于日志文件生成系統不變式(temporal invariants)，僅針對系統中出現的事件的時序邏輯進行描述，而不關注系統的狀態變遷，模型精化過程中模型間一致性檢測方法通過模擬系統的狀態變遷反映出系統的行為屬性，使得使用系統行為屬性的方法來進行模型間的一致性檢測成為可能。ProMiner是模型與代碼間的雙向一致性檢測工具，把模型中生成的抽象測試用例具體化后運行于代碼，通過比較執行結果是否一致，進而找出不一致，但這種方法關注于模型與代碼間的一致性檢測，并不針對于模型與模型之間的一致性檢測，模型精化過程中模型間一致性檢測方法旨在檢測模型與模型間的不一致。綜上所述，目前的屬性抽取方法并不能很好地解決模型間行為方面的一致性檢測問題，如何從抽象模型中抽取出反映系統行為的具體的系統屬性亟需新的方法。

2 模型間一致性檢測方法

本文提出使用系統行為屬性的方法來驗證模型精化過程中模型間的一致性，以此來彌補傳統一致性檢測方法的不足。精化后的模型除了滿足模型基本條件(例如語法、語義、結構方面的正確性，無死鎖性，不變式保持性等)外，還需要滿足精化前模型的行為屬性，即反應模型行為方面的屬性在精化后的模型中也是成立的，可以通過驗證精化后的模型是否滿足這些系統屬性來進行一致性檢測。同時，由于模型間精化關系錯綜復雜模型精化前后同一子模塊的重命名、子模塊一對多或多對一的精化關系時而出現，單純地從精化前模型抽取系統行為無法完全代表精化后模型應該遵守的行為屬性，為此我們對系統行為屬性進一步分析處理，更新成為適用于精化后模型的系統行為屬性。為了驗證該方法的有效性，本文選取Event-B語言模型，并使用ProB作為模型檢測工具，系統屬性使用可直接用于模型檢測的線性時序邏輯(LTL)，實驗結果表明使用此方法可以有效找出模型精化前后的大多數不一致行為。

2.1 基本流程

模型精化過程中模型間的一致性檢測工作流程如圖1所示。首先對精化前的模型生成抽象測試用例，再從這些抽象測試用例中抽取系統行為屬性，經過從精化后模型中抽取的精化關系的更新后，使用這些系統屬性去驗證精化后的模型是否滿足，如果不滿足則說明精化前后的模型存在行為方面的不一致，需要根據反例路徑修改精化后的模型，再迭代進行驗證，直到精化后的模型能夠滿足這些系統屬性為止。

圖1 模型間一致性檢測工作流程

2.2 一個例子

為了更容易理解此方法的工作原理，這里使用一個簡單的燒水壺的小例子。該系統把燒水壺抽象為兩層模型(Kerttle0,Kettle1)，Kettle1在初始模型Kettle0的基礎上進行精化，將Kettle0中的lid_open_1和lid_open_2合并為lid_open，將Kettle0中的lid_is_close重命名為lid_close，將Kettle0中的add具體刻畫為add(1)、add(2)、add(3)；將Kettle0中的pour具體刻畫為pour(1)、pour(2)、pour(3)。具體以Kettle1為例系統模型可以描述為以下事件和狀態：事件主要包括打開壺蓋(lid_open)、關閉壺蓋(lid_close)、打開開關(button_on)、關閉開關(button_off)、加水add(int)、倒水pour(int)；狀態主要包括壺蓋開(lid=open)、壺蓋關(lid=closed)、開關開(button=on)、開關關(button=off)、水的高度(fill_height)。該燒水壺模型可以使用Event-B形式化描述如下：

Machine:=Kettle0

State:={lid∈{open,close},button∈{on,off},fill_height∈{0,1,2,3}};

Event:={INITIALIZATION,lid_open_1,lid_open_2,lid_is_close,button_on,button_off,add(int),pour(int)}

Machine:=Kettle1

State:={lid∈{open,close},button∈{on,off},fill_height∈{0,1,2,3}};

Event:={INITIALIZATION,lid_open,lid_close,button_on,button_off,add(1),add(2),add(3),pour(1),pour(2),pour(3) }

2.3 抽象測試用例生成

模型間一致性檢測方法首先以測試用例的形式來描述精化前模型的系統的行為變化，針對該模型生成抽象測試用例。這里的測試用例是在ProMiner的基礎上產生的，每條抽象測試用例對應于模型中的一條執行路徑。抽象測試用例中記錄執行路徑中狀態遷移的觸發事件和每一個狀態遷移發生后系統的到達狀態，即(eventname,state)。測試用例以TestCase=list(, , …)的形式表示，即一組由<觸發事件，系統到達狀態>組成的線性表。以2.2節中的初始模型(Kettle0)為例，其一條測試用例如下所示。這條測試用例表示初始狀態為(lid=closed,fill_height=0,maximum=3,button=off)，執行事件lid_open后狀態變為(lid=open,fill_height=0,maximum=3,button=off)。

ProMiner生成的測試用例

2.4 系統行為屬性抽取

模型間一致性檢測方法使用系統行為屬性來描述各層模型間抽象到具體的關系，通過模擬模型的執行反映出系統狀態遷移的遷移及其觸發事件，進而抽取出系統行為屬性。Event-B系統模型中Event事件為一組代表系統狀態遷移的遷移，形如：Event:=any(var)where(condition)then(action)end，即對參數集var在前置條件集condition下可執行action。由此可見，針對每個事件(event)，事件的發生需要在滿足前置條件集(condition)后才可以執行某些操作(action)，結合上一步生成的抽象測試用例，系統的行為屬性可以描述為事件(event)的前后置條件，系統行為屬性抽取算法如下所示：

input: testSuite

output: LTL Set

define Step pair(Event, State)

define TestCase list(Step1,Step2,...)

define TestSuite list(TestCase1,TestCase2,....)

initilisationState={};preState={};postState={}; lastStep=(Event,State)

procedure extract the pre-condition and post-condition about every event to LTL

foreach TestCase in TestSuite do

foreach Step in TestCase do

if (Step.Event==INITILISATION) then

preState=null

//初始化只有后置條件沒有前置條件

postState=Step.State

//記錄當前step，方便找出下一個event的preState

lastStep.Event.name=INITILISATION

lastStep.State=Step.State

initilisationState.add(postState);

//記錄以LTL形式寫入LTL Set中

write ″G{postState}″ to LTL Set

else then

//當前event的preState為上一個event的postState

preState=lastStep.State

postState=Step.State

lastStep.Event.name=Step.Event.name

//記錄當前step

lastStep.State=Step.State

preState.add(preState,Step.Event.name)

//前置條件

write ″G({preState}=>e(Step.Event.name))″ to LTL Set

postState.add(preState,Step.Event.name,postState);

//后置條件

write″G(({preState}&e(Step.Event.name))=> X{postState})″ to LTL Set

end

end

end

end procedure

其中測試用例集TestSuite可分為多條測試用例TestCase，每條測試用例可分為若干個步驟Step，每個步驟Step又可以分為二元組(Event,State)，preState為前置條件集合，postState為后置條件集合，由于當前事件的前置條件即為上一個事件的后置條件，所以這里定義lastStep記錄當前事件和狀態，類型為Step類型。首先針對初始化事件，由于初始化事件不需要前置條件，故只需找出后置條件即可。針對其他事件，前置條件即為上一個事件的后置條件(即lastStep.State)，后置條件即為當前事件的狀態(即Step.State)，針對每個事件(Step.Event)分別把它的前置條件和后置條件以LTL的形式寫入LTL集合中(LTL Set)，即為抽取出的系統行為屬性的集合。這些形如G({preState}=>e(Step.Event.name))，G(({preState} & e (Step.Event.name))=>X{postState})的行為屬性中G(globally)意為總是成立，X(next)意為下一個狀態，在前置條件集preState狀態下可以發生某個事件(event)，在某個事件(Step.Event.name)的前置條件集(preState)和發生這個事件操作情況下則這個事件的下一個狀態集為postState。2.3節中展示了一個這樣的測試用例，首先初始化操作(關閉蓋子，水高為0，開關為關)，然后執行打開蓋子操作(lid=open)，則Step1 = < INITIALISATION,{lid=closed, fill_height=0, maximum=3, button=off}>，Step2 = 。可以看出，針對這一條測試用例，lid_open的前置條件集就是lid_open事件的上一個事件(INITIALISATION)發生后的State，lid_open的后置條件集就是lid_open事件發生后的State，為此針對事件lid_open可以生成如下兩條LTL：

前置條件：G(({lid= closed & fill_height= 0 & maximum= 3 & button= off})=>e(lid_open))

后置條件：G((({lid= closed & fill_height= 0 & maximum= 3 & button= off}) & e(lid_open))=>X({lid= open & fill_height= 0 & maximum= 3 & button= off}))

即在滿足前置條件集壺蓋關(lid=closed)、水高為0 (fill_height=0)、最大高度為3 (maximum=3)、開關關 (button=off)的條件下可以發生打開壺蓋(lid_open)操作，在滿足這些前置條件集且執行了打開壺蓋操作(e(lid_open))后的后置條件為壺蓋開(lid=open)、水高為0(fill_height=0)、最大高度為3(maximum=3)、開關關(button=off)，這里事件lid_open執行的操作就是令lid:=open。

上述系統屬性抽取算法可以檢測出的不一致類型主要分為以下三種：

1) 初始狀態不一致

這種不一致發生在模型初始化過程中，初始化不一致會被認為反映的不是同一個模型需求。例如以2.2節中燒水壺模型為例，存在如下初始化不一致：

精化前模型初始化：{button:=off & lid:=closed & fill_height:=0}

精化后模型初始化：{button:=off & lid:=open & fill_height:=0}

可以看出精化前模型初始化時蓋子為關閉狀態(lid:=closed)，而精化后初始化蓋子為打開狀態(lid:=open)。

2) 前置條件不一致

如上文中所提到的模型中事件可以表示為：Event:=any(var) where(condition) then(action) end，其中condition規定了事件執行需要滿足的前置條件集，只有滿足前置條件才能執行這一操作，例如以2.2節中燒水壺模型為例，存在如下前置條件不一致：

精化前模型：G(({lid=closed & fill_height=0 & maximum=3 & button=off})=>e(lid_open_1))

精化后模型：G(({lid=closed & fill_height=0 & maximum=3 & button=on})=>e(lid_open))

可以看出精化前模型此事件的前置條件中開關狀態為關(button:=off)才可以執行打開蓋子操作，而精化后開關狀態為開(button:=on)時才可以執行此操作，精化后模型定義了和精化前不一致的行為。

3) 后置條件不一致

后置條件規定了執行這個操作之后系統所到達的狀態，以此來間接檢測event中的action，通過觀測action操作前后狀態的對比可以得到action操作產生了哪些行為，從而從操作前后的對比可以檢測是否有不一致行為發生。例如以2.2節中燒水壺模型為例，存在如下后置條件不一致(即事件中的操作不一致)：

精化前模型：G((({lid=open & fill_height=2 & maximum=3 & button=off}) & e(lid_open_1) => X({lid=closed & fill_height=2 & maximum=3 & button=off }))

精化后模型：G((({lid=open & fill_height=2 & maximum=3 & button=off}) & e(lid_open) => X({lid=closed & fill_height=3 & maximum=3 & button=off }))

可以看出精化前模型并沒有對水高(fill_height)產生影響，而精化后的模型此事件的操作影響了水高(由2變為3)，所以認為精化前后的模型定義了不一致行為。

2.5 精化關系抽取

在實際的模型精化的過程中，由于模型的復雜性和建模者的行為習慣，導致精化前后模型之間事件(Event)關系的錯綜復雜，有時會發生精化后的模型的同一個事件名稱發生了變化，也可能會發生精化后事件合并和事件拆分的情況，如果不做處理的話，不一致檢測時會把不同事件名稱的事件當作不同的事件。為此在抽取上述LTL后還需要進行進一步的處理，檢測是否有事件名稱變化、事件合并、事件拆分的情況發生，如果有則用精化后的新事件名稱代替精化前的舊事件名稱，精化關系抽取和名稱替換算法如下所示：

input: model’s bum; LTL Set

//bum為精化后模型詳細信息

output: new LTL Set

define target list(eventName1,eventName2…)

define label list(eventName1,eventName2….)

define Relation pair(label,target)

//label為當前模型eventName，target為精化前模型eventName

define Event list(Relation1,Relation2...)

define bum list(Event1,Event2,...)

define LTL Set list(LTL1,LTL2,...)

define LTL list(event1,event2...)

relationMapping={Target,Label};

procedure find the different refine name in the model

foreach Event of after-refinement model in bum do

foreach Relation in Event do

if (label!=target) then

//精化前后名稱不同

relationMapping.add(target,label);

end

end

end

end procedure

procedure replace the old eventName by new eventName

foreach LTL in LTL Set do

foreach event in LTL do

foreach element in the relationMapping do

//存在精化前后名稱不同(包括多對一)的事件

if (Step.Event.name==relationMapping.Target)then

//用精化后名稱替換精化前名稱

event.replace(Step.Event.name,relationMapping.Label);

end

end

end

end

end procedure

該算法主要針對以下三種事件精化類型：

1) 事件名稱變化

由于建模者的設計習慣不一樣，有可能會發生精化后的模型的同一個事件用了不同名稱，雖然建模過程中并不主張這種設計方法，但這種情況還是會時有發生。例如精化前事件lid_is_close精化后為lid_close，系統屬性抽取是針對事件的，如果事件名稱不一樣會被認為不是同一個事件。為此在抽取系統的行為屬性后還需要判斷是否有這種情況發生。具體可以通過掃描精化后的模型的詳細信息是否存在refine前后事件名稱不同的情況，如果有，則用精化后的事件名稱替換精化前的事件名稱。例如2.2節燒水壺實例中，針對精化前模型Kettle0中事件lid_is_close，精化后模型Kettle1中重命名為lid_close，則替換后的LTL為：G(({lid= open & fill_height= 0 & maximum= 3 & button= off})=>e(lid_close))，G((({lid= open & fill_height= 0 & maximum= 3 & button= off}) & e(lid_close))=>X({lid= closed & fill_height= 0 & maximum= 3 & button= off}))。

2) 事件合并

事件合并是指精化前模型中的兩個或兩個以上的事件精化后合并為一個事件，事件合并的前提條件是事件執行的操作是相同的(即action相同)，合并后的事件為原事件的并集。針對這種情況也是通過掃描精化后模型的詳細信息判斷是否存在一個事件refine多個事件，如果有則用refine后的事件名稱替換精化前的這多個事件名稱。例如2.2節燒水壺實例中精化前模型中的事件。

lid_open_1:

condition: lid:=closed, button:=off;

action: lid:=open;

lid_open_2:

condition: lid:=closed, button:=on;

action: lid:=open;

精化后合并為一個事件：

lid_open:

condition: lid:=closed;

action: lid:=open;

這里可以合并的原因是無論開關打開或關閉都可以執行打開壺蓋(lid=open)的操作，合并后又由于button只有兩個狀態開和關，這里兩個狀態下都可以進行操作故可認為打開蓋子和開關狀態無關，可把(button:=on)∨(button:=off)這個condition忽略不計。通過掃描精化后模型的信息可以得出lid_open_1和lid_open_2精化后合并為一個事件lid_open，則針對原始LTL中lid_open_1和lid_open_2兩個事件的LTL：

合并前為：G(({lid= closed & fill_height= 0 & maximum= 3 & button= off})=>e(lid_open_1))，G(({lid= closed & fill_height= 0 & maximum= 3 & button= on})=>e(lid_open_2))。

合并后為：G(({lid= closed & fill_height= 0 & maximum= 3 & button= off})=>e(lid_open))，G(({lid= closed & fill_height= 0 & maximum= 3 & button= on})=>e(lid_open))。

3) 事件拆分

由于事件拆分全由開發人員的建模習慣決定，拆分關系錯綜復雜，很難做到完全自動化，我們目前主要針對含有參數的事件的拆分進行處理。精化后可能會把精化前含有參數的事件進行拆分，以此來更詳細地反映模型細節，例如2.2節燒水壺實例中：事件add拆分為add(1)、add(2)、add(3)，ProMiner在生成抽象測試用例時默認會把事件的參數加進去，即生成的LTL中事件名稱即為add(1)、add(2)、add(3)，故上述算法沒有對這種特殊情況進行處理也還是可以檢測一部分這種類型的不一致。若含有參數的事件在精化后并沒有產生事件拆分的操作(即還為add)，則可參考事件名稱變化的處理方法，把add(1)、add(2)、add(3)重命名為add。

2.6 系統行為屬性驗證

使用上述步驟中抽取出的系統行為屬性對精化后的模型進行一致性檢測，利用模型檢測生成的反例路徑定位模型中不一致的位置。延續2.2節中的燒水壺實例，對精化后模型Kettle1檢測生成的一條反例路徑形如圖2所示。圖2中的反例路徑對應的一條LTL輸入為：G((({lid= closed & fill_height= 3 & maximum= 3 & button= off}) & [lid_open])=>X({lid= open & fill_height= 3 & maximum= 3 & button= off}))，圖中T表示為真(True)，F表示為假(False)，U表示不確定(Undetermined)。通過圖2中F結點的指向關系可以看出不一致發生在lid_open這個事件的后置條件中，即圖2中最下面Next({lid= open & fill_height= 3 & maximum= 3 & button= off})這一行中，Next表示事件的后置條件，所以可以具體定位到Kettle1模型lid_open事件的action中。可以發現，在執行lid_open這個事件操作時，精化后的模型和精化前的模型存在不一致行為，精化前Kettle0中lid_open事件的action為lid:=open，精化后Kettle1中lid_open事件的action為lid:=closed，在驗證lid_open這個事件的過程中lid的狀態產生了不一致，建模者可以通過修改此不一致迭代進行驗證。

圖2 燒水壺示例反例路徑

3 實驗分析

如上所述，傳統的模型間一致性檢測方法只對模型自身的語法、語義、結構方面的正確性、死鎖和不變式保持性進行檢測，而很難檢測系統行為方面的一致性，為此提出使用系統行為屬性的方法來驗證模型精化過程中模型間的一致性。為分析該方法的有效性，選取了三個系統Celebrity、Kettle、VOBC進行一致性檢測，其中Celebrity是著名的“名人”示例系統，以人物之間的關系作為輸入信息，輸出符合條件的名人。Kettle是文中使用的燒水壺示例系統。VOBC[32,33]系統是車載控制器模型系統，系統中一列(或幾列)列車在一條軌道線上運行，主要負責完成車載ATP(列車自動防護)/ATO(列車自動運行)功能，該系統的目的是提供安全的列車運行。

為驗證模型間一致性檢測方法的有效性，對上述三個系統人工注入不一致，通過對比發現，模型間一致性檢測方法可以檢測到ProB檢測不到的不一致行為，如表1所示。 從表1中可以看出，模型間一致性檢測方法檢測出的不一致不僅包含了ProB檢測出的不一致，而且還檢測出了ProB檢測不出的許多不一致。檢測結果中的不一致類型和模型各層間的不一致結果如表2所示，分別詳細說明了檢測出的不一致在三種類型(初始狀態不一致、前置條件不一致、后置條件不一致)中的個數，以及不一致在各個模型間的分布情況。

表1 模型間一致性檢測實驗結果

表2 不一致類型和各層間分布

模型精化過程中模型間一致性檢測方法可以檢測出的不一致類型主要為初始狀態不一致、前置條件不一致、后置條件不一致三種類型，而沒有發現的不一致主要集中在以下區域：

1) 含有參數的事件

沒有發現的含有參數的事件不一致主要表現為某些局部變量。其中局部變量類似于Event:=any(var) where(condition) then(action) end中的var，ProMiner在生成測試用例時，覆蓋所有的參數取值空間會導致狀態爆炸[9-12]，故ProMiner只會取一些較容易出錯或出現次數頻繁的參數作為觀察對象，而有些不一致行為恰恰需要這些變量的某些取值才能觸發，故而若生成的測試用例中不包括觸發不一致行為的取值的話，則此不一致不會被發現。例如2.2節燒水壺實例中：精化前模型事件加水操作add(fill_height)中fill_height的取值范圍為(1…100)，生成的測試用例中只有參數為(1,28,50,79,100)時的情況，若不一致發生在參數為30時，這時此不一致將不會被發現。

2) 新增變量和事件(event)

由于模型精化過程中模型間一致性檢測是使用精化前模型的系統屬性來驗證精化后的模型，針對精化后模型新增的變量和事件是不適用的，但是由于是使用相鄰兩層間的模型進行一致性檢測(即使用第0層模型的系統屬性去驗證第1層模型，使用第1層模型的系統屬性去驗證第2層模型，以此類推)，這種差異不會一直持續擴大化。在以后的研究中，會持續探索此問題的解決方法。值得提出的是，由于模型精化過程中模型間一致性檢測是從初始模型(即第0層模型)中開始，一般情況下認為初始模型是正確的，但是若初始模型存在錯誤，則這個錯誤有可能在接下來的模型精化中一直存在，雖然這也是一種錯誤，但是此方法旨在檢測模型之間的不一致，若初始模型和第1層模型中存在不一致行為，初始模型出錯還是第1層模型出錯取決于建模者的決策。

4 結 語

模型檢測和模型精化是基于模型驅動開發方法的常用技術，自提出至今在多方面都有了一定的發展，對模型進行一致性檢測能夠有效幫助建模者建立正確合理的模型。為了驗證模型精化過程中行為描述的一致性，提出使用系統行為屬性的方法來驗證模型精化過程中模型間的一致性。以抽象測試用例為手段描述模型間抽象到具體的對應關系，用系統中觸發事件的相關前后置條件描述系統行為，參照模型間的精化關系，提取系統行為屬性，并結合模型檢測結果，有效幫助建模者定位模型不一致所在。

實驗結果表明使用此方法能夠有效找出大多數的不一致行為。在今后的研究工作中，將打算使用系統其他方面的屬性或結合代碼級別的一致性檢測方法來輔助進行一致性檢測研究，以使得該方法得到進一步的完善。

[1] 王帥強，馬軍，王海洋，等.基于遺傳規劃的行為模型精化方法[J].計算機研究與發展，2008，45(11)：1911-1919.

[2] Back R J R.Refinement calculus, part ii: parallel and reactive programs[C]//proceedings on Strpwise refinement of distributed systems: models, formalisms, correctness, REX workshop, pp. 67-93, New York, NY, USA, 1990. Springer-Verlag New York, Inc.

[3] 曾紅衛，繆淮扣. 構件組合的抽象精化驗證[J].軟件學報，2008，19(5):1149-1159.

[4] Chen Z, Liu Z, Ravn A P, et al. Refinement and verification in component-based model-driven design[J].Science of Computer Programming,2009,74(4):168-196.

[5] 劉靜，何積豐，繆淮扣.模型驅動架構中模型構造與集成策略[J].軟件學報，2006，17(6)：1411-1422.

[6] 張康康，趙建華. MDA模型轉換工具的研究[J].計算機應用與軟件，2009，26(8)：122-124,135.

[7] 蔣楠，丁祥武. 基于模型驅動元數據管理策略的研究[J].計算機應用與軟件，2012，29(1)：188-190.

[8] Schmidt D C. Guest Editor’s Introduction: Model-Driven Engineering[J].Computer,2006,39(2):25-31.

[9] Clarke E, Grumberg O, Long D. Model checking[M].Cambridge, MA, MIT Press, 1999.

[10] 賀亞博，郝克剛，葛瑋.模型檢測在軟件需求分析及設計中的應用[J].計算機應用與軟件，2009，26(4)：128-130.

[11] Christel Baier, Joost Pieter Katoen. Principles of Model Checking (Representation and Mind Series)[M].Cambridge, Massachusetts, The MIT Press, 2008.

[12] 林惠民, 張文輝. 模型檢測: 理論、方法與應用[J].電子學報，2002,30:1907-1912.

[13] Axelsson R, Hague M, Kreutzer S, et al. Extended Computation Tree Logic[J].Lecture Notes in Computer Science, 2010:6397:67-81.

[14] 蘇開樂，駱翔宇，呂關鋒. 符號化模型檢測CTL[J].計算機學報，2005，28(11)：1798-1806.

[15] Huth M, Ryan M. Logic in Computer Science: Modeling and reasoning about systems[M].Cambridge University Press, 2010.

[16] Ernst M D,Perkins J H,Guo P J,et al. The Daikon system for dynamic detection of likely invariants[J].Science of Computer Programming,2007,69(1):35-45.

[17] Ernst M D, Cockrell J, Griswold W G, et al. Dynamically discovering likely program invariants to support program evolution. IEEE Trans Softw Eng[J].IEEE Transactions on Software Engineering,2001,27(2):99-123.

[18] Chen Xiao. Performance Enhancements for a Dynamic Invariant Decector[M].Masters thesis, MIT Department of Electrical Engineering and Computer Science, Cambridge, MA, Feb,2007.

[19] Perkins J H, Ernst M D. Efficient Incremental Algorithms for Dynamic Detection of Likely Invariants[J].Acm Sigsoft Software Engineering Notes,2004:23-32.

[20] Beschastnikh I, Brun Y, Schneider S. Leveraging existing instrumentation to automatically infer invariant-constrained models[C]//Proceedings of the 19thACM SIGSOFT Symposium and the 13thEuropean Conference on Foundations of Software Engineering. New York, USA:ACM Press,2011:267-277.

[21] Ivan Beschastnikh, Yuriy Brun, Michael D Ernst, et al. Bandsaw: Log-powered test scenario generation for distributed systems[C]//SOSP Work In Progress, Cascais, Portugal, October 24-26, 2011.

[22] Ivan Beschastnikh, Jenny Abrahamson, Yuriy Brun, et al.Synoptic: Studing Logged Behavior with Inferred Models[C].FSE’11, September 5-9, 2011, Szeged, Hungary.

[23] Ivan Beschastnikh, Yuriy Brun, Michael D Ernst, et al. Mining Temporal Invariants from Partially Ordered Logs[C].SLAML’11, October 23, 2011, Cascais, Portugal.

[24] Sigurd Schneider, Ivan Beschastnikh, Slava Chernyak,et al.Synoptic: Summarizing System Logs with Refinement[C]//Workshop on Managing System via Log Analysis and Machine Techniques (SLAML’10), Vancouver , BC, Canada, October 3,2010.

[25] Abrial J R. Modeling in Event-B: system and software engineering[M].Cambridge University Press, 2010.

[26] Abrial J R. The B-book: assigning programs to meanings[M].Cambridge University Press, New York, NY, USA, 1996.

[27] 蘇雯. 基于Event-B的混合系統形式化：理論與實踐[D].上海：華東師范大學軟件學院，2013.

[28] Jean Raymond Abrial, Michael Butler, Stefan Hallerstede, et al.Rodin: an open toolset for modeling and reasoning in Event-B[J].International Journal on Software Tools for Technology Transfer (STTT),2010,12(6):447-466.

[29] Rodin website. http://wiki.event-b.org/index.php/rodin_platform.

[30] Leuschel M, Butler M. ProB: A model checker for B[M]//FME 2003: Formal Methods. Springer Berlin Heidelberg,2003:855-874.

[31] Dinca I, Ipate F, Mierla L, et al. Learn and test for Event-B-a Rodin plugin[M]//Abstract State Machines, Alloy, B, VDM, and Z. Springer Berlin Heidelberg, 2012:361-364.

[32] Platzer A.Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics[D].Springer, Heidelberg,2010.

[33] Su W, Abrial J R, Zhu H. Complementary Methodologies for Developing Hybrid Systems with Event-B[M]//Formal Methods and Software Engineering Springer Berlin Heidelberg,2012:230-248.

[34] 葛徐駿，王玲，徐立華，等.ProMiner:系統性質驅動的雙向一致性檢驗框架[J].軟件學報，2016(7):1757-1771.

[35] 王戟，李宣東.形式化方法與工具專刊前言[J].軟件學報，2011,22(6):1121-1122.

RESEARCH OF CONSISTENCY CHECKING BETWEEN MODELS IN THE PROCESS OF MODEL REFINEMENTS

Wang Ling Xu Lihua

(DepartmentofComputerScienceandTechnology,EastChinaNormalUniversity,Shanghai200241,China)

During model refinement process, traditional consistency checking techniques tend to focus on the syntax and semantics of the models, their structural correctness, as well as deadlock and invariants retention, while ignoring the behavior consistency. To address the problem, the system behaviors are captured via the form of system property and model checking techniques are utilized to check the consistencies among system models. Firstly, the pre-refinement model is analyzed and abstract test cases are generated from it, important system behaviors are then extracted as system properties and expressed as linear temporal logic (LTL); Secondly, these system properties are updated based on the refinement relationships, which are extracted between pre and after refinement models. Thirdly, the extracted system properties are checked over the after-refinement model. The possible inconsistency positions could be found through the counter-example path.The early experimental results show that most of the inconsistency could be found between pre and after refinement models using this approach.

Model refinement Model checking Consistency checking Property extract Linear temporal logic

2015-10-28。國家自然科學基金項目(61502170)；上海市科委自然科學基金項目(13ZR1413000)。王玲，碩士生，主研領域：軟件分析和測試，形式化方法。徐立華，副教授。

TP311

A

10.3969/j.issn.1000-386x.2016.11.001