基于UML的实时系统建模及顺序图时间约束研究

摘要

随着信息技术的高速发展，实时系统的应用范围变得越来越广泛。要正确的设计出一个实时系统，就要在分析实时系统的早期给出实时系统的正确模型。统一建模语言UML正是用来对复杂系统进行建模的。UML模型分为静态结构模型和动态行为模型两类，静态模型关注系统的结构信息，而动态结构模型关注系统的行为信息。一般而言，UML动态行为模型往往更加复杂和重要。使用UML为实时系统的动态行为建模的方法是本文的研究内容之一。 同时，实时系统的实时行为可以用时间约束条件来描述，但UML是一种图形化的语言，它的语义使用自然语言描述的，存在不精确性。因此，形式化的语义就成了UML的一个迫切需求。把UML和形式化语言进行融合，通过形式化的方法来弥补UML语义上的不足，给出实时行为方面模型的精确语义，也是本文的研究重点。 本文工作主要内容归纳如下： 首先，对UML2新增图之一交互概观图进行了研究，提出了一种基于交互概观图对实时式系统进行建模的方法，并通过一个具体建模实例来说明这种方法。此方法与通常的建立动态行为模型方法相比更加直观和全面，能从整体上把握系统的动态行为。 然后，在前人研究的基础上给出了UML顺序图和时间约束属性相关方面的形式化定义，包括简单顺序图、带组合片段的顺序图和时间约束同一性。并对顺序图扩充时间性质以便于描述实时系统。精确的形式化描述是整个研究的基石，后面的分析和验证都基于该形式化描述。 最后，对带组合片段的顺序图满足时间约束同一性的定理进行了证明，并以此定理为基础对带时间约束属性的UML顺序图提出了一种验证算法，判断其是否符合某些时间约束属性。带时间约束属性的顺序图为实时系统的建模提供了便利，通过检验系统的行为是否满足某种时间约束属性，能够提高实时系统的安全性。