基于时序描述逻辑的UML状态图语义研究

摘要

统一建模语言(Unified Modeling Language)UML简洁、直观，便于建模人员之间的交流与沟通，适用于软件开发的各个阶段。然而，UML缺乏精确的形式化语义，难以对它所描述的系统进行形式化分析和一致性检验。描述逻辑具有很强的表达和可判定推理能力，但基本的描述逻辑只能表示静态领域的知识，无法对具有动态和时序特征的知识进行描述。时序逻辑包含大量的时序算子，可以对静态和动态领域的知识进行描述，但它的推理能力不是很强。
　　 针对上述问题，本文对基本的描述逻辑进行时序扩展，然后用扩展后的描述逻辑，即用时序描述逻辑TDLs(Temporal Description Logics)对UML状态图进行形式化研究，提高UML状态图语义描述的精确性。本文的主要研究工作包括：
　　 1.UML和描述逻辑的异同点。比较了UML和描述逻辑的异同点，包括：静态、动态、共享、可扩展性、继承、封装、类之间的关系、类和属性的层次，以及推理特性。
　　 2.描述逻辑的时序扩展。针对基本的描述逻辑无法对具有动态与时序特征的知识进行描述的问题，考虑采用时序算子对基本的描述逻辑进行扩展，得到既可以表示静态知识，又可以对动态和时序知识进行描述的时序描述逻辑，给出了扩展后的语法、语义、定义及公理。
　　 3.UML状态图的形式化。状态图是UML重要的行为图之一，通过对状态图进行分析，将UML状态图映射为时序描述逻辑表达式，给出了映射规则，并通过一个实例说明了映射过程，检验了方法的可行性，对形式化后的表达式也进行了正确性检验。

目录

文摘

英文文摘

论文说明:图表目录

声明

第1章绪论

1.1研究背景与意义

1.2形式化方法的研究

1.2.1软件形式化的研究方法

1.2.2 UML形式化的研究方法

1.3当前存在的主要问题

1.4本文的主要工作

1.5本文的组织结构

第2章UML状态图形式化的研究现状

2.1用Petri网形式化UML状态图

2.2用时序逻辑语言XYZ/E形式化UML状态图

2.3用B语言形式化UML状态图

2.4用动态描述逻辑形式化UML状态图

2.5本章小结

第3章UML和描述逻辑

3.1面向对象模型与UML

3.1.1面向对象的基本思想

3.1.2面向对象模型的基本概念与特征

3.1.3面向对象的建模语言——UML

3.2描述逻辑基础

3.2.1描述逻辑的发展

3.2.2描述逻辑的语法、语义及基本体系

3.3本章小结

第4章描述逻辑的扩展与状态图的形式化

4.1 UML与描述逻辑的比较

4.2基本描述逻辑的扩展

4.2.1描述逻辑的动态扩展

4.2.2描述逻辑的时序扩展

4.2.3扩展后的可满足性规则

4.2.4扩展后的Tableau算法

4.2.5 Tableau算法的基本性质

4.3状态图的形式化及实例分析

4.3.1映射规则

4.3.2实例分析

4.4本章小结

总结与展望

参考文献

致 谢

附录A攻读硕士期间发表的学术论文