论文部分内容阅读
实时系统的正确性不仅取决于计算的逻辑结果,而且依赖于系统运行的时间。如何确保实时系统的正确性和可靠性是软件研究人员广泛关注的问题。UML (united modeling language)是一种通用的标准化的建模语言,适用于软件开发的各个阶段,但其缺乏精确的语义信息,因此难以直接进行验证。而形式化方法(formal methods)提供了一种严格精确的数学方法,通常被用于软件设计阶段,分析系统的可靠性。因此,通过将UML模型转换到形式化模型进行模型验证,是保证软件质量的有效手段。MARTE (modeling and analysis of real time and embedded systems)是OMG组织专门针对嵌入式实时系统的建模规范,用于取代原有的UML-SPT (uml profile for schedulability, performance and time)。时间自动机(the timed automata)是一种成熟的实时系统模型验证工具,它扩展了自动机理论,并为实时系统行为的创建和分析提供了一种形式化方法。模型驱动工程(model-driven engineering,简称MDE)的理念伴随着人们对软件系统的不断抽象,而逐渐受到重视。它以模型为首要软件制品(software artifact),其主要的研究方向为(元)建模和模型转换。元-元模型体系(meta-metamodel architecture)根据抽象度的不同,划分出元-元模型(meta-metamodel)、元模型、模型(和实例)等三(四)个层次,其中抽象度低的模型遵从抽象度高的元模型。元-元模型是元模型的“根”,它为所有遵从它的元模型之间的桥接,提供了一种共同的方式。本文给出了一种基于MDE的UML/MARTE模型到时间自动机模型的转换方法,它包含三个步骤:首先通过时间自动机的元建模,将其引入到MDE的元-元模型体系中;然后,定义UML/MARTE和时间自动机元模型之间的映射规则,并由模型转换语言的支撑平台实施转换过程;最后,按照模型检测工具的输入格式,将转换得到的时间自动机模型进行重写,以便进行模型验证。本文先后探讨了:1.如何基于MDE,将UML/MARTE模型转换到时间自动机验证模型。它关注两个方面:1)如何将时间自动机集成到元-元模型体系;2)如何实现基于元模型的模型转换。2.通过对时间自动机元建模,将其集成到元-元模型体系。集成的目的是为了让时间自动机和UML/MARTE拥有共同的“根”和操作集,从元模型层实现两者的相互理解。3.通过定义元模型层的映射规则,实现UML/MARTE模型到时间自动机模型的转换。转换过程实际上是由映射规则定义语言的支持平台执行。由于模型检测工具通常由自己的输入格式,因此,整个模型转换过程还附带了从模型到文本描述转换的过程。