论文部分内容阅读
在软件工程中，具有决定意义的是系统建模。建模是为了更好的理解和构造系统，并可以提供简化和复用的机会。通常软件系统的分析与设计都是通过建模来完成的。
随着计算机应用软件的大型化和复杂化，不同程序之间的交互和集成变得越来越困难。为此，OMG提出了MDA(ModelDrivenArchitecture，模型驱动的体系结构)技术。MDA将系统模型分为两种：PIM(PlatformIndependentModel，与平台无关的模型)和PSM(PlatformSpecificModel，与平台有关的模型)。MDA的核心是基于映射的模型转换，它定义了PIM和PSM模型之间的四种映射关系：PIM到PIM，PIM到PSM，PSM到PSM，PSM到PIM。
在MDA中，PIM和PSM都使用UML来描述。UML是一种可视化的通用的面向对象建模语言，它被用于描述和构建复杂的软件系统。UML自1997年被OMG接纳为标准以来，得到了工业界、科技界和应用界的广泛支持，目前已经成为建模语言事实上的标准。因此，现在针对软件建模的研究主要集中在UML领域。
由于UML的语义是用自然语言描述的，存在不精确性，因此通过定义UML模型的形式化语义来提高UML语言的精确性成为当前研究的一个热点。UML模型分为静态模型和动态模型两类，静态模型关注系统的结构信息，而动态模型关注系统的行为信息。一般而言，UML动态模型往往更加复杂和重要。本文在MDA框架下，针对UML中的两种主要的动态模型——顺序图和状态图——的语义进行了深入研究，提出了一系列模型转换和验证的方法，主要的工作有：
(1)给出了顺序图和状态图在语法上和语义上的形式化描述，并对它们进行了扩充。我们在顺序图上添加了时间约束，使之便于描述实时系统。为了描述顺序图之间的关系，我们引入了高级顺序图的概念。对于状态图，我们区分了简单状态图和复杂状态图，并提出了系统状态图的概念。
(2)研究了顺序图的时间一致性检查算法。带时间约束的顺序图能够很好的描述实时系统和分布式系统中的时间性质。作为一种规约语言，顺序图的时间约束之间可能相互矛盾。我们设计了一个顺序图的时间一致性的检验算法，分析了两种时间一致性：一般顺序图的时间一致性和高级顺序图的时间一致性。
(3)研究了从顺序图中生成状态图的算法。我们设计了一个从一组UML顺序图中合成状态图的算法，合成的过程基本上是自动完成的，只需要很少的用户交互。该算法为软件开发过程中从需求到设计的过渡提供了有力的支持。
(4)研究了顺序图和状态图之间的一致性检查算法。顺序图和状态图都描述了系统的动态行为，它们所包含的信息存在冗余，因而就会出现不一致的情形。我们从事件顺序的角度出发，通过检查顺序图的运行轨迹中的事件序列是否会在系统状态图的某个执行中出现，来判断顺序图和状态图之间的一致性。
(5)形式化语义有着清晰和准确的含义，但对于最终用户而言，往往显得过于复杂而难以使用。因此，基于以上的形式化工作，我们设计和开发了一个UML模型转换和验证的工具。该工具是整个MDA支撑工具的一部分。它集成了(2)、(3)和(4)中的算法，提供了丰富的图形界面和友好的用户交互方式，具有较强的实用性。