基于UML的形式化规范说明研究

摘要

软件的规范说明阶段(specification phase)对于软件整体开发过程来说是一个非常重要的阶段,它可以被认为是需求分析的一部分.用自然语言来说明软件需求的优点是直观易懂、方便交流,但是会带来很多弊病,如二义性和不精确等.因此必须研究需求分析和规范说明技术以获得一致、完备和准确的软件规范说明书.形式化需求分析和软件规范说明技术就是在需求获取的基础上用建立系统的逻辑模型,从而对复杂实际问题进行分析和抽象、消除错误、去粗取精,最终将用户需求转化为软件规范说明的方法.软件系统的需求分析和规范说明阶段的多种方法和技术已被提出.这些方法大体上可被分为两类:形式化方法和非形式化方法.非形式化方法一般是采用图表的方式来描述系统.UML就是一种非形式化的方法,该方法是目前比较流行的软件工程开发方法,它对软件整体开发过程提供了一套有用的模型.UML方法已被广泛的应用于软件开发过程的各个阶段.被证明是一种行之有效的方法.但是它有所有非形式化方法所共有的缺点:表达的不严格和不精确,并且和规范的一致性和完整性不能被形式证明.该文为了解决UML的以上缺点,根据UML和谓词转换,以一阶逻辑和时序逻辑为基础提出一种面向对象的形式化规范说明方法,并给出一组和UML相对应的数学模型.该文的方法吸收了UML和一般形式化方法的优点,具有数学的严谨性和精确性,并且更加易于理解和表达.该软件规范说明方法的研究目标是使其能够最终实现目标代码的自动与半自动生成和程序的自动与半自动验证.

目录

文摘

英文文摘

独创性声明及学位论文版权使用授权书

第一章绪论

1.1形式化方法的重要意义

1.2形式化方法和形式化规格说明语言的发展状况

1.3形式化方法的研究内容

1.4形式化方法与软件可靠性

1.5软件逐步精化方法

第二章统一建模语言UML

2.1UML简介

第三章系统

3.1语法与语义

第四章谓词转移图对UML状态转移图的模拟

第五章模态逻辑模型

第六章时序逻辑语义

第七章程序精化思想

7.1传统程序观点

7.2抽象程序观点

7.3精化

第八章类型

8.1类型的分类

8.1.1按抽象层次来分类：

8.1.2按类型中元素的数目来分类：

8.1.3按类型的结构分类：

8.2基本类型

8.3构造类型

8.3.1幂集

8.4包

8.4.1包与集合间的转换

8.5序列

8.5.1序列概括

8.5.2复合

8.5.3子序列

8.5.4子段

8.5.5前缀

8.5.6后缀

8.5.7分配运算符

8.6函数

8.6.1函数的限制与协限制

8.7关系

第九章具体范例

第十章结论

参考文献

发表论文及参加科研情况说明

致谢