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

Research on Model Checking Formal Language Object-Z

作　　者：吴彩燕[1] 

机构地区：[1]苏州市职业大学计算机工程学院,江苏苏州215104

出　　处：《苏州市职业大学学报》2015年第3期29-35,共7页Journal of Suzhou Vocational University

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

摘　　要：Object-Z是一种用于表示面向对象系统规约的高层抽象语言,由于缺乏自动验证工具的支持,很难建立直接证明由Object-Z表示的面向对象系统规约正确性,成为Object-Z被广泛采用的最大障碍.模型检测是一种验证系统规约正确性的自动化技术.使用模型检测工具SPIN验证Object-Z描述的正确性,把Object-Z的规约转换成标记转换系统,然后把标记转换系统转换为SPIN的输入语言Promela,使用线性时序逻辑刻画Object-Z中的历史不变式.通过对订票系统类的Object-Z描述的验证,结果表明该方案具有可行性.Object-Z is a high-level abstract language used to represent the specification of the object-oriented 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.

关 键 词：模型检测 OBJECT-Z SPIN 时序逻辑 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]