-
题名基于Object-Z的形式化验证方法
被引量：7
- 1
-
-
作者
文志诚
缪淮扣
张新林
-
机构
上海大学计算机学院
-
出处
《计算机科学》
CSCD
北大核心
2007年第5期247-251,共5页
-
基金
国家自然科学基金(60373072)
上海市教委第四期重点学科建设基金资助
-
文摘
定理证明是一种形式化验证技术,也是形式化方法的重要组成部分,它能从形式规格说明中推理出应具备的性质与属性,从而可以对规格说明进行形式验证。Object-Z是形式规格说明语言Z的面向对象扩充,基于集合论与数理逻辑,具有严密的逻辑性,适合精确地描述大型软件系统,并且可以对其形式规格说明进行推理。本文首先给出了基于Object-Z规格说明的定理证明验证方法,接着用Object-Z描述了一个电梯操作系统的实例,在此基础上给出了其形式规格说明的定理证明方法来进行形式化验证。
-
关键词
OBJECT-Z
形式化验证
前后置条件
状态空间
电梯操作系统
-
Keywords
Object-Z, Formal verifihation, Pre-＆Post-condition, State space, Operation system of elevator
-
分类号
TP312
[自动化与计算机技术—计算机软件与理论]
-
