基于动态逻辑的UML模型一致性检验

摘要

在基于UML的软件开发过程中，各种UML图形从不同侧面描绘着所开发的软件系统，这些图形之间存在着信息的重叠，从而导致UML模型的一致性问题。UML模型的一致性问题也是建模过程中一个重要并且需要解决的问题。 KeY Tool是一个支持形式化规范和代码验证的工具，该工具基于动态逻辑对程序和形式化规范进行分析和验证，然而该工具并不支持在设计阶段对UML模型进行一致性检验。作为KeY Fool的基础，动态逻辑不仅具备描述程序设计语言的能力，而且能够描述UML/OCL中的动态概念。因此，研究利用动态逻辑来解决UML 模型的一致性问题具有理论意义和应用价值。 本论文首先对UML模型存在的一致性问题进行综述，在此基础上深入分析已有的方法，即Greg提出的利用动态逻辑来检验UML模型一致性的方法中存在的问题。Greg的方法只针对某一特定简单的UML模型进行设计，而本论文从一般UML模型的基本要素出发来分析模型转换的方法，解决了原有方法中存在的一些问题。并且，原有方法只支持类图、顺序图和状态图的检验，本论文对该方法进行扩充，增加了OCL规范与其他UML图形之间的一致性检验。 通过案例分析表明，改进和扩充后的方法不但能检验出更多UML图形之间的一致性问题，而且能检验出OCL约束与其他UML图形之间的一致性问题。

目录

文摘

英文文摘

声明

第1章绪论

1.1研究背景及意义

1.2国内外的研究现状

1.3本文的研究动机和研究思路

1.4本文的主要工作

1.5论文的组织

第2章动态逻辑简介

2.1模态逻辑简介

2.2动态逻辑简介

2.3本章小结

第3章UML模型的一致性问题

3.1一致性问题的分类及其产生的原因

3.2一致性问题的解决途径

3.3本章小结

第4章模型转换

4.1系统动态行为在DL中的描述

4.2确定DL的基调

4.3类图的转换

4.4 OCL约束的转换

4.5状态图的转换

4.6顺序图的转换

4.7本章小结

第5章实例研究

5.1类图及其DL公式

5.2 OCL约束及其转换

5.3状态图及其DL公式

5.4顺序图及其DL公式

5.5本章小结

第6章一致性检验

6.1一致性检验过程

6.2本章小结

总结与展望

参考文献

致谢