论文部分内容阅读
统一建模语言(UML)是对象管理组织(OMG)提出的-Y2218070它主要用在以模型为驱动的软件开发过程的建模阶段。自UML提出之日起,它便处在不断的修缮和扩充过程中,修缮主要集中在语义上,而扩充则表现在各个方面,其中,为增强UML对实时系统的建模能力,OMG在2009年给出了一个对UML进行了扩充的规范,即UML Profile for MARTE:Modeling and Analysisof Real-rime Embedded Systems(简称MARTE)。顺序图是UMI和MARTE中的一类动态图,它的语法用类图表示,语义则用非形式化的自然语言描述,这种非形式化的语义易使用户与开发人员对系统的动态行为产生歧义。因此给出UML和MARTE中定义的顺序图的形式化语义是一个待解决的问题。 把模型转换成代码是以模型作为驱动的软件开发过程的一个环节,在此之前开发人员需对模型的正确性进行验证。与模拟、测试和演绎验证不同,模型检查是一种能覆盖所有路径的自动验证技术。为了用该技术对顺序图构造的模型的正确性进行验证,OMG借鉴了模型转换的思想,即将依照UML或MARTE设计的模型(记为A)转换成形式化模型(记为B),其中B具有完备的验证方法和工具并能够模拟A的行为。 由于可达性、活性和无死锁性等性质都无法在顺序图中得到直接验证,所以利用模型转换,我们将顺序图转换成能模拟其行为的形式化模型。借助形式化模型已有的验证工具,我们可以验证顺序图的各项性质。本文的主要工作包括以下三个方面: ·选择形式化模型Petri网作为目标模型,将库所/变迁网扩充并将扩充后的petri网-LPN4SD-作为目标模型。把UML顺序图中的组合片段(包括Assert和Negate类型的组合片段)转换成LPN4SD。将LPN4SD的变迁加入时间区间(记作TLPN4SD)并给出TLPN4SD的弱语义。证明了在弱语义下,TLPN4SD的可达性、有界性和覆盖性是可判断的。最后定义了基于弱语义的时间迁移系统(TTS:time transition system)的产生算法,用TPN-TCTL描述MARTE顺序图对应的TLPN4SD的属性并展开验证; ·给出了MARTE顺页序图的形式化定义,将TTS扩展成TTS4SD以从两个方面—事件间的迁移和组合片段间的迁移—描述MARTE顺序图的行为,给出了MARTE顺页序图到TTS4SD的转换方法,在此基础上同样展开验证和精化工作: ·将MARTE顺页序图直接转换成MARTE CCSL描述的模型,并证明了两者的互模拟关系。CCSL与上述模型—Petri网和时间迁移系统一的不同在于,它和MARTE顺页序图都是MARTE规范中定义的模型。 本文对已有方法的改进主要表现在以下方面:我们给出的模型大都是已有的经典形式化模型的扩展形式,扩展主要集中在语法的定义上,这些模型模拟了顺序图的动态行为;另外,我们给出的顺序图的形式化定义弥补了UML和MARTE中用类图描述顺序图的语法的不足之处;根据本文的转换规则,我们还给出了顺序图到目标模型的转换算法,这样给定顺序图的形式化定义后,根据转换算法,就可以自动生成目标模型;最后,从顺序图到CCSL(Clock Constraint Specification Language)模型的转换方法扩大了MARTE规范的应用范围,即将其应用从建模阶段扩大到验证阶段。