模型精化过程中模型间一致性检测研究

王 玲 徐立华

(华东师范大学计算机科学技术系 上海 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