形式语言Object-Z的模型检测研究

吴彩燕

(苏州市职业大学 计算机工程学院，江苏 苏州 215104)

形式语言Object-Z的模型检测研究

吴彩燕

(苏州市职业大学 计算机工程学院，江苏 苏州 215104)

Object-Z是一种用于表示面向对象系统规约的高层抽象语言，由于缺乏自动验证工具的支持，很难建立直接证明由Object-Z表示的面向对象系统规约正确性，成为Object-Z被广泛采用的最大障碍.模型检测是一种验证系统规约正确性的自动化技术.使用模型检测工具SPIN验证Object-Z描述的正确性，把Object-Z的规约转换成标记转换系统，然后把标记转换系统转换为SPIN的输入语言Promela，使用线性时序逻辑刻画Object-Z中的历史不变式.通过对订票系统类的Object-Z描述的验证，结果表明该方案具有可行性.

模型检测；Object-Z；SPIN ；时序逻辑

模型检测[1]被认为是一类证明系统性质的有效技术，由于具有工具的支持，极大地提高其可应用性.模型检测工具已经被广泛应用于硬件、协议和并发、实时软件的验证.当今面向对象技术比较成熟，而面向对象系统的模型检测方法却很少得到关注，更不用说开发专门用于它们的模型检测工具.

Object-Z[2]是形式化描述语言Z[3]的面向对象扩展，适合于获取基于状态系统的性质.然而，缺乏自动验证工具的支持成为Object-Z被广泛采用的最大障碍.如果能够使用工具检查Object-Z描述的错误或验证系统性质，这会极大地发挥Object-Z的潜力.

研究给出了模型检测Object-Z描述的方法.把Object-Z描述转换成标记转换系统[4]，然后把标记转换系统转换为SPIN[5]的输入语言Promela，再使用线性时序逻辑[6]刻画Object-Z中的历史不变式，以此验证Object-Z描述的正确性.

试验选择LTS有多个理由：①由于Object-Z是一种高层抽象语言，没有直接用于它的模型检测工具，所以必须把它转换成一种中间表示形式以使用现有的模型检测工具.LTS则是可以用于多种模型检测工具的中间表示形式.②Object-Z是基于状态的描述语言，跟LTS的描述机制非常相似，这样就会使得它们之间的转换相对直接和简单，而且能很好保持Object-Z的语义.

近年来，关于Object-Z的模型检测工作也得到了一些关注.集成了CSP与OZ[7]，把OZ与ASM相结合[8]，它们的工作只能分别用于专门的模型检测工具FDR和SMV[9]，直接把Object-Z描述转换成SMV程序，没有考虑转换过程中的语义保持[10].把Object-Z转换成转换系统，虽然保持了Object-Z的语义，而且也能用于多种模型检测工具，但没有考虑操作组合问题[11].模型检测工具PAT其功能包含了模型检测TCOZ，主要思想类似于文献[7]，不同点是使用LTS定义进程的语义，使用集成的模型检测工具完成模型检测过程.

1 Object-Z

Object-Z是形式化描述语言Z的面向对象扩展，Object-Z中最主要的结构是类的定义，其中封装了状态模式和相关的操作模式.

一个Object-Z的类用带有名字的框表示，该名字就是类名.类中可以包括局部变量和常量的声明，以及至多一个状态模式和初始状态模式，还可以包括0个或多个操作.状态模式的声明称为状态变量，谓词声明称为类的不变式.类的不变式约束了状态变量的可能取值.初始状态模式指定了状态模式的初始值.一个操作要么是操作模式，要么是包含已有的操作和模式操作符的模式表达式.操作由前置和后置条件约束.订票系统类的Object-Z描述见图1：

图1 订票系统类的Object-z

图1中State是状态变量，指定订票系统类可能的状态.ticketnum是一个常量，表示现有机票的数量.INIT指定的是该类的初始模式，即对状态变量State和常量ticketnum初始化.Query和Book操作表示客户可以通过旅游代理进行查询和订购机票.RequestTicket操作表示旅游代理可以直接向航空公司购票.只有当前机票数大于0时，客户才能订票成功，否则失败.

Object-Z允许把由与类相关的历史不变式指定的活性性质描述为时序逻辑公式.历史不变式约束了类的状态变化的历史集合.用线性时序逻辑表示历史不变式.本研究中历史不变式表示客户订票时，只要当前票数大于0时，就能成功订票，否则订票失败.

2 标记转换系统(LTS)

使用标记转换系统来描述Object-Z类的语义.Object-Z类的语义是类的对象能够经历的计算的集合.标记转换系统是计算集合的紧凑表示，因而是Object-Z类的语义合适的表示形式.而且已经出现了大量检查LTS所表示模型性质的验证工具.下面给出其具体定义.

定义1 标记转换系统是一个四元组(S，s0，L，T)，其中：S是状态的集合；s0是初始状态；L=EVE×ACT×GUD是标记集合，其中EVE、ACT、GUD分别是事件集合、动作集合、监视条件集合；T⊆S×L×S是转换关系.

3 模型检测Object-Z描述

Object-Z的描述可以看成是抽象的状态机.它的类的对象可以通过操作产生状态序列.使用LTS定义这些状态序列的紧凑表示.一个Object-Z类的定义主要包括如下元素：

3．1 从Object-Z描述到LTS

3.1 ．1 转换规则

常量定义：常量在Object-Z的一开始就定义，它的值在转换过程中保持不变，所以在从Object-Z描述到LTS的转换过程可以不作考虑.

状态模式：状态模式里面定义了一些局部变量和状态变量，可以直接转换成LTS中的状态.设var和state分别是在状态模式中定义的局部变量和状态变量，定义函数Π：var×state→S，它把(var，state)对映射到LTS的状态集合.

初始状态模式：初始状态模式为状态模式中定义的局部变量和状态变量给定了初始值，可以把它直接转换成LTS中的初始状态.即Π：var0×state0→s0，把var和state的初始值对(var0，state0)映射成LTS的初始状态.

状态转换：在Object-Z中状态转换由操作实现，操作可以通过改变△列表中变量的值实现状态转换.对于△列表中的变量组成的对，只要有一个变量的值进行修改，那么就可以从一个状态转换到另一个新状态.例如(var，state)对中var的值变为var′，那么(var，state) →(var′，state)，对于上述对可以转换到三个不同的新状态.

操作：一个操作要么是操作模式，要么是包含已有的操作和模式操作符的模式表达式.操作由前置和后置条件约束，表示对象的状态变化情况.对于只是操作模式的操作，本研究把它转换成LTS中的事件，操作的前置条件和后置条件分别转换为LTS中的监视条件和动作.定义函数F：Op→Seq EVE，把Object-Z中的操作集合Op定义为LTS中的事件序列.函数P：Pre(Op)→GUD把操作的前置条件定义为LTS中的监视条件集合.函数Q：Post(Op)→Seq ACT把操作的后置条件定义为LTS中的动作序列.

对于包含有模式操作符的组合操作而言，分下面四种情况讨论：

设LE是LTS中所有使能的转换的集合，使用t2＜t1表示转换t1的优先级高于转换t2.在组合操作中每个独立的操作都直接转换为LTS中的一个转换.

1) 合取操作.两个操作Op1和Op2可以合取，当且仅当它们没有相同的输入输出变量，即它们对应的转换是协调的.下面使用LTS定义合取操作的语义.

RS：after(ai)/before(aj)其中revar(ai)表示对出现在Opi中的主变量重命名，这样的主变量与出现在Opi+1中的非主变量具有相同的名字.如果没有这样的变量，那么revar(ai)为null.after(ai)/before(ai+1)表示用重命名的变量在Opi之后和在Opi+1之前替换Opi+1后置条件中的非主要变量.如果revar(ai)为null，那么after(ai)/before(ai+1)为null.

如果每个操作Opj的前置条件满足，那么将导致状态变化，并产生相应的动作.对于组合操作而言，如果它们的前置条件的合取成立，那么将顺序执行各个操作，依次从第一个操作的源状态转换到最后一个操作的目标状态，并生成动作序列.

2) 选择操作.选择操作的语义定义如下：

其中k∈{i，j}.如果操作Opi比Opj有更高的优先级，并且它的前置条件满足，那么执行该操作对应的转换并生成相应的动作.

3) 并行操作.并行操作与合取操作相类似，唯一不同的是并行操作需要通过输入和输出变量通信，所以除了要求它们对应的转换是协调外，还要求它们之间的输入输出变量是一致的.设函数input：Op→Parameter用来获取操作Op的输入变量，对于两个并行操作Opi和Opj来说，它们的输入输出变量是一致的，当且仅当(output(Opi) input(Opj))∧(output(Opj) input(Opi)).并行操作的语义定义与合取操作的语义定义相同.

C：constraint(output(ti)) S：output(ti)/input(tj)，其中output(ti)/input(tj) 用Opi的输出变量替换Opj的输入变量.

4) 顺序操作.顺序操作是两个操作的顺序组合，要求第一个操作的目标状态要与第二个操作的源状态相同.而且第一个操作的输出变量要与第二个操作的输入变量相同.操作Op1和操作Op2可以顺序组合，当且仅当(target(Op1)=source(Op2))∧(output(Op1)=input(Op2)).其中target(Op1)表示Op1的目标状态.顺序操作的语义定义如下：

其中:·表示序列的连接操作；S-1表示input(tj)/output(ti).

3.1.2 订票系统类的LTS表示

根据前面的转换规则，把订票系统类的Object-Z描述按照下列步骤转换成LTS.订票系统类的Object-Z描述按照转换规则转换后得到的LTS表示，如图2和图3所示.

图3 订票系统类的另一个LTS表示

在状态模式中有一个局部变量ticketnum和状态变量State，所以(ticketnum，State)对组成了LTS中的状态集合S.

在初始模式中ticketnum=100，State=init，因此初始状态s0=(ticketnum=100，init).

订票系统类里面总共有三个操作Book，Query和RequestTicket.RequestTicket操作根据当前票数是否大于0有两种情况，可以看成选择操作.

因为(target(Book)=source(RequestTicket))∧(output(Book)=input(RequestTicket))，所以操作Book和RequestTicket是顺序操作；因为source(Book RequestTicket)∩source(Query)≠∅，所以Book RequestTicket和Query所对应的转换是复合转换；又因为(read(Book RequestTicket)∩write(Query)=∅)∧(write(Book RequestTicket)∩read(Query)=∅)，所以它们是合取操作.

操作名直接转换为LTS中的事件，前置条件和后置条件分别转换为监视条件和动作.

在图2和图3中：tn，c，a，s，f，Q，B，RT分别是ticketnum，client，agent，success，failure，Query，Book，RequestTicket的缩写.由于各个操作的原子性，可知上述的两个LTS是等价的.

3．2 从LTS到Promela

状态：LTS中的状态可以用Promela中的mtype{}来声明，(var，state)这样的对可以定义为一个新的状态变量.

输入输出变量：在转换中的监视条件和动作中包含的输入输出变量，用通道chan来定义.对于复合转换中的输入输出变量，定义为同步通道.

转换：转换中的监视条件和动作在Promela中分别定义为前置条件和后置条件，前置条件放在if…fi中作为布尔表达式，用atomic来表示转换的原子性.以ready状态到wait状态的转换为例来说明.

state==ready-＞

if

：：c?=B-＞atomic{a!=RT；state=wait；}

fi

整个LTS用active proctypeprocessname{}来声明，其中processname表示进程名.

4 实例验证

通过SPIN验证性质□(client?book∧ticketnum＞0=＞client!success)∨□(client?book∧┓(ticketn um＞0) =＞client!failure).验证结果显示上述性质满足订票系统类的Object-Z描述.验证结果见图4.

图4 证明结果

5 结论

详细介绍了一种验证Object-Z描述的方法并给出了转换规则.使用模型检测工具SPIN验证Object-Z描述的正确性，给出从LTS到Promela的转换过程，把Object-Z描述转换成LTS这种能够用于多种模型检测工具的中间表示形式，在转换过程中保持了Object-Z的语义.最后以验证订票系统类的Object-Z描述来说明其可行性.

虽然给出了从Object-Z描述到LTS的转换规则，但相应的转换算法仍需要在今后的工作中去实现.本研究中的历史不变式是用线性时序逻辑公式表示的，如果以其他形式表示，对其进行验证有待进一步思考和研究.

[1] CLARKE E M，GRUMBERG O，PELED D A.Model checking cambridge[M].MA：The MIT Press，2000.

[2] SMITH G.The Object-Z specification language[M].Netherlands：Advances in Formal Methods，Kluwer Academic Publishers，2000.

[3] WOODCOCK J C P，DAVIES J.Using Z：specification，proof and refinement[M].London：Prentice Hall International Series in Computer Science，1996.

[4] 董威，王戟. UML状态机的模型检验方法[J]. 计算机工程与科学，2001，23(6)：7-11.

[5] BEN-ARI M.Principles of the spin model checker[M].Berlin：Springer-verlag，2008.

[6] YONEDA T，SCHLINGLOFF H.On model checking for petri nets and a linear-time temporal logic[J/OL].http：//www.informatik.uni-bremen. de/～hs/.

[7] KASSEL G，SMITH G.Model checking Object-Z classes：some experiments with FDR[C]//In 8th Asia-Pacific Software Engineering Conference(APSEC2001).Macau：IEEE Computer Society Press，2001.

[8] WINTER K，DUKE R.Model checking Object-Z using ASM[C]//In the third international conference on Integrated Formal Methods(IFM2002). Turku，LNCS：2002：162-184.

[9] PREIBUSCH S，KAMMULLER F.Checking the TWIN elavator system by translating Object-Z to SMV[C]//In 12th International Workshop on Formal Methods for Industrial Critical Systems(FMICS2007).Berlin，LNCS：2008：38-55.

[10] GRUER P，HILAIRE V，KOUKAM A.Verification of Object-Z specifications by using transition systems：application to the radiomobile network design problem[C]//In the Third International Conference on Fundamental Approaches to Software Engineering(FASE2000).Berlin，LNCS：2000：222-236.

[11] LIU Y.Model checking concurrent and real time systems：The PAT approach[D].Singapore：The Doctor Degree Thesis，National University of Singapore，2001.

(责任编辑：李 华)

Research on Model Checking Formal Language Object-Z

WU Cai-yan
(School of Computer Engineering，Suzhou Vocational University，Suzhou 215104，China)

Object-Z is a high-level abstract language used to represent the specification of the objectoriented system.For lack of support of automatic verification tools，it is difficult to verify the correctness of the specification of the object-oriented system represented by Object-Z.Model checking is such an automatic verification technique.This paper verifies the correctness of the Object-Z specification using model checking tool-SPIN，which translates the Object-Z specification into label transition system (LTS) firstly，and then converts the LTS format into the input language Promelaof SPIN.Subsequently，the history invariant in Object-Z is described by Linear Temporal Logic (LTL).Through verifying the Object-Z specification of the booking system class，the results show that this method is feasible.

model checking；Object-Z；SPIN；temporal logic

TP311

A

1008-5475(2015)03-0029-07

2015-05-10；

2015-06-09

苏州市职业大学青年基金资助项目(2014SZDQ06)

吴彩燕(1975-)，女，江苏苏州人，主要从事教学管理、计算机软件方向研究.