王 玲 徐立華

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

?

模型精化過(guò)程中模型間一致性檢測(cè)研究

王 玲 徐立華

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

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

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

0 引 言

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

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

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

1 背景介紹

1.1 模型檢測(cè)

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

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

1.2 Event-B模型

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

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

1.3 一致性檢測(cè)

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

1.4 屬性抽取

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

2 模型間一致性檢測(cè)方法

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

2.1 基本流程

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

圖1 模型間一致性檢測(cè)工作流程

2.2 一個(gè)例子

為了更容易理解此方法的工作原理，這里使用一個(gè)簡(jiǎn)單的燒水壺的小例子。該系統(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具體刻畫(huà)為add(1)、add(2)、add(3)；將Kettle0中的pour具體刻畫(huà)為pour(1)、pour(2)、pour(3)。具體以Kettle1為例系統(tǒng)模型可以描述為以下事件和狀態(tài)：事件主要包括打開(kāi)壺蓋(lid_open)、關(guān)閉壺蓋(lid_close)、打開(kāi)開(kāi)關(guān)(button_on)、關(guān)閉開(kāi)關(guān)(button_off)、加水a(chǎn)dd(int)、倒水pour(int)；狀態(tài)主要包括壺蓋開(kāi)(lid=open)、壺蓋關(guān)(lid=closed)、開(kāi)關(guān)開(kāi)(button=on)、開(kāi)關(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 抽象測(cè)試用例生成

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

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

模型間一致性檢測(cè)方法使用系統(tǒng)行為屬性來(lái)描述各層模型間抽象到具體的關(guān)系，通過(guò)模擬模型的執(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，即對(duì)參數(shù)集var在前置條件集condition下可執(zhí)行action。由此可見(jiàn)，針對(duì)每個(gè)事件(event)，事件的發(fā)生需要在滿足前置條件集(condition)后才可以執(zhí)行某些操作(action)，結(jié)合上一步生成的抽象測(cè)試用例，系統(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

//初始化只有后置條件沒(méi)有前置條件

postState=Step.State

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

lastStep.Event.name=INITILISATION

lastStep.State=Step.State

initilisationState.add(postState);

//記錄以LTL形式寫(xiě)入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

其中測(cè)試用例集TestSuite可分為多條測(cè)試用例TestCase，每條測(cè)試用例可分為若干個(gè)步驟Step，每個(gè)步驟Step又可以分為二元組(Event,State)，preState為前置條件集合，postState為后置條件集合，由于當(dāng)前事件的前置條件即為上一個(gè)事件的后置條件，所以這里定義lastStep記錄當(dāng)前事件和狀態(tài)，類(lèi)型為Step類(lèi)型。首先針對(duì)初始化事件，由于初始化事件不需要前置條件，故只需找出后置條件即可。針對(duì)其他事件，前置條件即為上一個(gè)事件的后置條件(即lastStep.State)，后置條件即為當(dāng)前事件的狀態(tài)(即Step.State)，針對(duì)每個(gè)事件(Step.Event)分別把它的前置條件和后置條件以LTL的形式寫(xiě)入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è)這樣的測(cè)試用例，首先初始化操作(關(guān)閉蓋子，水高為0，開(kāi)關(guān)為關(guān))，然后執(zhí)行打開(kāi)蓋子操作(lid=open)，則Step1 = < INITIALISATION,{lid=closed, fill_height=0, maximum=3, button=off}>，Step2 = 。可以看出，針對(duì)這一條測(cè)試用例，lid_open的前置條件集就是lid_open事件的上一個(gè)事件(INITIALISATION)發(fā)生后的State，lid_open的后置條件集就是lid_open事件發(fā)生后的State，為此針對(duì)事件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)、開(kāi)關(guān)關(guān) (button=off)的條件下可以發(fā)生打開(kāi)壺蓋(lid_open)操作，在滿足這些前置條件集且執(zhí)行了打開(kāi)壺蓋操作(e(lid_open))后的后置條件為壺蓋開(kāi)(lid=open)、水高為0(fill_height=0)、最大高度為3(maximum=3)、開(kāi)關(guān)關(guān)(button=off)，這里事件lid_open執(zhí)行的操作就是令lid:=open。

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

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

這種不一致發(fā)生在模型初始化過(guò)程中，初始化不一致會(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)，而精化后初始化蓋子為打開(kāi)狀態(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))

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

3) 后置條件不一致

后置條件規(guī)定了執(zhí)行這個(gè)操作之后系統(tǒng)所到達(dá)的狀態(tài)，以此來(lái)間接檢測(cè)event中的action，通過(guò)觀測(cè)action操作前后狀態(tài)的對(duì)比可以得到action操作產(chǎn)生了哪些行為，從而從操作前后的對(duì)比可以檢測(cè)是否有不一致行為發(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 }))

可以看出精化前模型并沒(méi)有對(duì)水高(fill_height)產(chǎn)生影響，而精化后的模型此事件的操作影響了水高(由2變?yōu)?)，所以認(rèn)為精化前后的模型定義了不一致行為。

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

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

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

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

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

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

end

end

end

end

end procedure

該算法主要針對(duì)以下三種事件精化類(lèi)型：

1) 事件名稱變化

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

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

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

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

使用上述步驟中抽取出的系統(tǒng)行為屬性對(duì)精化后的模型進(jìn)行一致性檢測(cè)，利用模型檢測(cè)生成的反例路徑定位模型中不一致的位置。延續(xù)2.2節(jié)中的燒水壺實(shí)例，對(duì)精化后模型Kettle1檢測(cè)生成的一條反例路徑形如圖2所示。圖2中的反例路徑對(duì)應(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)。通過(guò)圖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è)事件的過(guò)程中l(wèi)id的狀態(tài)產(chǎn)生了不一致，建模者可以通過(guò)修改此不一致迭代進(jìn)行驗(yàn)證。

圖2 燒水壺示例反例路徑

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

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

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

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

表2 不一致類(lèi)型和各層間分布

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

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

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

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

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

4 結(jié) 語(yǔ)

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

實(shí)驗(yàn)結(jié)果表明使用此方法能夠有效找出大多數(shù)的不一致行為。在今后的研究工作中，將打算使用系統(tǒng)其他方面的屬性或結(jié)合代碼級(jí)別的一致性檢測(cè)方法來(lái)輔助進(jìn)行一致性檢測(cè)研究，以使得該方法得到進(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] 賀亞博，郝克剛，葛瑋.模型檢測(cè)在軟件需求分析及設(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] 林惠民, 張文輝. 模型檢測(cè): 理論、方法與應(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] 蘇開(kāi)樂(lè)，駱翔宇，呂關(guān)鋒. 符號(hào)化模型檢測(cè)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。國(guó)家自然科學(xué)基金項(xiàng)目(61502170)；上海市科委自然科學(xué)基金項(xiàng)目(13ZR1413000)。王玲，碩士生，主研領(lǐng)域：軟件分析和測(cè)試，形式化方法。徐立華，副教授。

TP311

A

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