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

摘要：

形式化方法让软件需求的规格说明变得更加简洁精确,但是它的抽象难懂让用户难以确定形式规格说明中所叙述的用户需求就是他们所期望的.另外,大多的规格说明语言都是不可执行的,因此人们采用一种动画模拟的方式,将形式规格说明转换成一种可模拟执行的形式,从而帮助用户和规格说明者确认形式规格说明是否与用户的非形式化需求相一致.通过分析比较形式规格说明的两种动画策略--形式化程序合成和结构模拟的优缺点,决定使用结构模拟技术将0bject-Z规格说明转换成SICStus Prolog可执行程序并加以执行,从而实现对Object-Z规格说明的确认.

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

所属期刊栏目：11

分类号：TP311.5(计算技术、计算机技术)

资助基金：中国科学院资助项目60373072;上海市教委资助项目02AK07

在线出版日期：2006-03-02（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：589-595