形式语言Object-Z的模型检测研究
吴彩燕
苏州市职业大学 计算机工程学院,江苏 苏州,215104
摘要：Object-Z是一种用于表示面向对象系统规约的高层抽象语言，由于缺乏自动验证工具的支持，很难建立直接证明由Object-Z表示的面向对象系统规约正确性，成为Object-Z被广泛采用的最大障碍。模型检测是一种验证系统规约正确性的自动化技术。使用模型检测工具SPIN验证Object-Z描述的正确性，把Object-Z的规约转换成标记转换系统，然后把标记转换系统转换为SPIN的输入语言Promela，使用线性时序逻辑刻画Object-Z中的历史不变式。通过对订票系统类的Object-Z描述的验证，结果表明该方案具有可行性。
关键词：模型检测Object-ZSPIN时序逻辑
分类号：TP311(计算技术、计算机技术)
资助基金：苏州市职业大学青年基金资助项目(2014SZDQ06)
论文发表日期：2015-01-01
在线出版日期：2025-08-15（本平台首次上网日期，不代表文献的发表时间）
页数：7( 29-35 )
英文信息