免费论文：UML动态行为模型的形式化描述和分析技术研究

自从1997年的提案被OMG组织采纳之后，到最新的UML2.0标准的推出，UML已经变成软件开发过程中广泛使用的标准建模语言。随着模型驱动体系结构（MDA）软件开发模式越来越受到重视，UML模型的形式化描述成为当今的研究热点。针对UML动态行为模型存在的复杂语义描述不够精确、模型可重用性较弱、模型可验证性手段不足等问题，论文基于Petri网，研究UML动态行为模型的形式化描述技术和安全性、活性、可达性和一致性等关键特性分析技术。论文成果能够有助于保证应用系统的建模质量，支持MDA开发过程，提高开发过程的自动化程度。论文首先对比分析典型的UML模型形式化描述手段，阐述了Petri网技术在UML模型的行为特征评价方面的优势。Petri网技术既有较强的形式化描述能力，又具有可视化的特点，能够保持与UML视图良好的过渡，并弥补UML视图非形式化描述的缺陷。它遵循事件发生需要前提条件触发、事件发生导致后继条件成立这一规则，可以用于描述状态变换和通信的系统需求，并作为UML状态图和顺序图特性分析及其一致性验证的基础。论文基于Petri网在以下三个方面开展研究工作：（1）在形式化描述方面，论文首先基于UML元模型，构造了一种能够刻画UML动态行为模型的结构特征和语义特征的Petri网模型框架，进而提出UML状态图的形式化模型SMPN和UML顺序图的形式化模型SDPN。借助层次化顺序自动机EHA完成非结构化状态图到结构化SMPN的转换，分析提出保证转换过程中状态图语义正确性的良构规则。为构造SDPN，论文分析其中的12种可重用交互片断语义，构造6种基本片段的Petri网模型。论文进一步提出了合成过程中的抽象、合并、同步化、化简等关键操作，构造了从UML顺序图到SDPN的映射规则。（2）在模型特性分析方面，论文基于Petri网分析了层次化SMPN、简单SDPN和条件SDPN的活性判定定理，构造了基于复合标识函数的可达标识图构造算法。对于状态图能否正常终止、指定状态是否可达、从指定状态是否可正常终止这三类典型可达性问题提出了基于可达标识图的解决方案。论文对模型的行为一致性和结构一致性进行了分析，并分类说明如何利用Petri网等价性理论分析模型的一致性。（3）在模型验证方面，论文介绍了自动化分析工具中的两个重要工具——一致性检测工具和系统仿真工具的实现方案。通过大型应用项目CPMSⅢ的开发实践，说明论文研究成果在提高应用系统的性能、改进系统结构、优化业务过程等实践中发挥了很好的作用。这表明论文提出的状态关联模型和交互关联模型具有实际应用价值和推广意义。实践证明，本文在UML动态行为模型描述与分析技术研究方面所取得的成果，不仅具有重要的理论研究意义，而且具有较大的实用价值，可以作为相关研究的参考和应用的基础。

来源：半壳优胜育转载请保留出处和链接！

本文链接：http://87cpy.com/274445.html