王 玲 徐立華

(華東師范大學(xué)計(jì)算機(jī)科學(xué)技術(shù)系 上海 200241)

?

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

王 玲 徐立華

(華東師范大學(xué)計(jì)算機(jī)科學(xué)技術(shù)系 上海 200241)

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

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

0 引 言

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

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

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

1 背景介紹

1.1 模型檢測

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

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

1.2 Event-B模型

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

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

1.3 一致性檢測

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

1.4 屬性抽取

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

2 模型間一致性檢測方法

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

2.1 基本流程

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

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

2.2 一個(gè)例子

為了更容易理解此方法的工作原理，這里使用一個(gè)簡單的燒水壺的小例子。該系統(tǒng)把燒水壺抽象為兩層模型(Kerttle0,Kettle1)，Kettle1在初始模型Kettle0的基礎(chǔ)上進(jìn)行精化，將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為例系統(tǒng)模型可以描述為以下事件和狀態(tài)：事件主要包括打開壺蓋(lid_open)、關(guān)閉壺蓋(lid_close)、打開開關(guān)(button_on)、關(guān)閉開關(guān)(button_off)、加水a(chǎn)dd(int)、倒水pour(int)；狀態(tài)主要包括壺蓋開(lid=open)、壺蓋關(guān)(lid=closed)、開關(guān)開(button=on)、開關(guān)關(guān)(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 抽象測試用例生成

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

ProMiner生成的測試用例

2.4 系統(tǒng)行為屬性抽取

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

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

//記錄當(dāng)前step，方便找出下一個(gè)event的preState

lastStep.Event.name=INITILISATION

lastStep.State=Step.State

initilisationState.add(postState);

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

write ″G{postState}″ to LTL Set

else then

//當(dāng)前event的preState為上一個(gè)event的postState

preState=lastStep.State

postState=Step.State

lastStep.Event.name=Step.Event.name

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

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

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

1) 初始狀態(tài)不一致

這種不一致發(fā)生在模型初始化過程中，初始化不一致會(huì)被認(rèn)為反映的不是同一個(gè)模型需求。例如以2.2節(jié)中燒水壺模型為例，存在如下初始化不一致：

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

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

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

2) 前置條件不一致

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

精化前模型：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))

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

3) 后置條件不一致

后置條件規(guī)定了執(zhí)行這個(gè)操作之后系統(tǒng)所到達(dá)的狀態(tài)，以此來間接檢測event中的action，通過觀測action操作前后狀態(tài)的對比可以得到action操作產(chǎn)生了哪些行為，從而從操作前后的對比可以檢測是否有不一致行為發(fā)生。例如以2.2節(jié)中燒水壺模型為例，存在如下后置條件不一致(即事件中的操作不一致)：

精化前模型：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)產(chǎn)生影響，而精化后的模型此事件的操作影響了水高(由2變?yōu)?)，所以認(rèn)為精化前后的模型定義了不一致行為。

2.5 精化關(guān)系抽取

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

input: model’s bum; LTL Set

//bum為精化后模型詳細(xì)信息

output: new LTL Set

define target list(eventName1,eventName2…)

define label list(eventName1,eventName2….)

define Relation pair(label,target)

//label為當(dāng)前模型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) 事件名稱變化

由于建模者的設(shè)計(jì)習(xí)慣不一樣，有可能會(huì)發(fā)生精化后的模型的同一個(gè)事件用了不同名稱，雖然建模過程中并不主張這種設(shè)計(jì)方法，但這種情況還是會(huì)時(shí)有發(fā)生。例如精化前事件lid_is_close精化后為lid_close，系統(tǒng)屬性抽取是針對事件的，如果事件名稱不一樣會(huì)被認(rèn)為不是同一個(gè)事件。為此在抽取系統(tǒng)的行為屬性后還需要判斷是否有這種情況發(fā)生。具體可以通過掃描精化后的模型的詳細(xì)信息是否存在refine前后事件名稱不同的情況，如果有，則用精化后的事件名稱替換精化前的事件名稱。例如2.2節(jié)燒水壺實(shí)例中，針對精化前模型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) 事件合并

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

lid_open_1:

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

action: lid:=open;

lid_open_2:

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

action: lid:=open;

精化后合并為一個(gè)事件：

lid_open:

condition: lid:=closed;

action: lid:=open;

這里可以合并的原因是無論開關(guān)打開或關(guān)閉都可以執(zhí)行打開壺蓋(lid=open)的操作，合并后又由于button只有兩個(gè)狀態(tài)開和關(guān)，這里兩個(gè)狀態(tài)下都可以進(jìn)行操作故可認(rèn)為打開蓋子和開關(guān)狀態(tài)無關(guān)，可把(button:=on)∨(button:=off)這個(gè)condition忽略不計(jì)。通過掃描精化后模型的信息可以得出lid_open_1和lid_open_2精化后合并為一個(gè)事件lid_open，則針對原始LTL中l(wèi)id_open_1和lid_open_2兩個(gè)事件的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) 事件拆分

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

2.6 系統(tǒng)行為屬性驗(yàn)證

使用上述步驟中抽取出的系統(tǒng)行為屬性對精化后的模型進(jìn)行一致性檢測，利用模型檢測生成的反例路徑定位模型中不一致的位置。延續(xù)2.2節(jié)中的燒水壺實(shí)例，對精化后模型Kettle1檢測生成的一條反例路徑形如圖2所示。圖2中的反例路徑對應(yīng)的一條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(xiàn)表示為假(False)，U表示不確定(Undetermined)。通過圖2中F結(jié)點(diǎn)的指向關(guān)系可以看出不一致發(fā)生在lid_open這個(gè)事件的后置條件中，即圖2中最下面Next({lid= open & fill_height= 3 & maximum= 3 & button= off})這一行中，Next表示事件的后置條件，所以可以具體定位到Kettle1模型lid_open事件的action中?？梢园l(fā)現(xiàn)，在執(zhí)行l(wèi)id_open這個(gè)事件操作時(shí)，精化后的模型和精化前的模型存在不一致行為，精化前Kettle0中l(wèi)id_open事件的action為lid:=open，精化后Kettle1中l(wèi)id_open事件的action為lid:=closed，在驗(yàn)證lid_open這個(gè)事件的過程中l(wèi)id的狀態(tài)產(chǎn)生了不一致，建模者可以通過修改此不一致迭代進(jìn)行驗(yàn)證。

圖2 燒水壺示例反例路徑

3 實(shí)驗(yàn)分析

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

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

表1 模型間一致性檢測實(shí)驗(yàn)結(jié)果

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

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

1) 含有參數(shù)的事件

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

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

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

4 結(jié) 語

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

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

[1] 王帥強(qiáng)，馬軍，王海洋，等.基于遺傳規(guī)劃的行為模型精化方法[J].計(jì)算機(jī)研究與發(fā)展，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] 曾紅衛(wèi)，繆淮扣. 構(gòu)件組合的抽象精化驗(yàn)證[J].軟件學(xué)報(bào)，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] 劉靜，何積豐，繆淮扣.模型驅(qū)動(dòng)架構(gòu)中模型構(gòu)造與集成策略[J].軟件學(xué)報(bào)，2006，17(6)：1411-1422.

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

[7] 蔣楠，丁祥武. 基于模型驅(qū)動(dòng)元數(shù)據(jù)管理策略的研究[J].計(jì)算機(jī)應(yīng)用與軟件，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] 賀亞博，郝克剛，葛瑋.模型檢測在軟件需求分析及設(shè)計(jì)中的應(yīng)用[J].計(jì)算機(jī)應(yīng)用與軟件，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] 林惠民, 張文輝. 模型檢測: 理論、方法與應(yīng)用[J].電子學(xué)報(bào)，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] 蘇開樂，駱翔宇，呂關(guān)鋒. 符號化模型檢測CTL[J].計(jì)算機(jī)學(xué)報(bào)，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的混合系統(tǒng)形式化：理論與實(shí)踐[D].上海：華東師范大學(xué)軟件學(xué)院，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:系統(tǒng)性質(zhì)驅(qū)動(dòng)的雙向一致性檢驗(yàn)框架[J].軟件學(xué)報(bào)，2016(7):1757-1771.

[35] 王戟，李宣東.形式化方法與工具專刊前言[J].軟件學(xué)報(bào)，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。國家自然科學(xué)基金項(xiàng)目(61502170)；上海市科委自然科學(xué)基金項(xiàng)目(13ZR1413000)。王玲，碩士生，主研領(lǐng)域：軟件分析和測試，形式化方法。徐立華，副教授。

TP311

A

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