Object-Z规格说明的结构模拟动画技术  

Structure Animation of Object-Z Specification

作　　者：朱江[1] 陈怡海[1] 缪淮扣[1] 

机构地区：[1]上海大学计算机工程与科学学院,上海200072

出　　处：《上海大学学报（自然科学版）》2005年第6期589-595,共7页Journal of Shanghai University:Natural Science Edition

基　　金：国家自然科学基金资助项目(60373072);上海市教委科学技术发展基金资助项目(02AK07)

摘　　要：形式化方法让软件需求的规格说明变得更加简洁精确,但是它的抽象难懂让用户难以确定形式规格说明中所叙述的用户需求就是他们所期望的.另外,大多的规格说明语言都是不可执行的,因此人们采用一种动画模拟的方式,将形式规格说明转换成一种可模拟执行的形式,从而帮助用户和规格说明者确认形式规格说明是否与用户的非形式化需求相一致.通过分析比较形式规格说明的两种动画策略———形式化程序合成和结构模拟的优缺点,决定使用结构模拟技术将Object-Z规格说明转换成SICStus Prolog可执行程序并加以执行,从而实现对Object-Z规格说明的确认.Formal method makes specification of software requirements more compact and more precise, but its abstract makes users very difficult to believe that the most specification languages specification described is what they desire. In addition, are not executable. Therefore animation of formal specification is used to translate the formal specification into an executable mode, and requirements. In this paper, two animation strategies structure simulation, are analyzed and compared then to validate the specification with user＇s informal of formal specification： formal program synthesis and Structure simulation is used to translate the Object-Z specification into SICStus Prolog program and execute it so as to validate the specification.

关 键 词：形式方法 形式规格说明 确认 动画模拟 OBJECT-Z PROLOG SICStus PROLOG 

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