论文部分内容阅读
随着实时软件在可靠性和安全性要求的广泛提高,以及实时系统在工业界的广泛应用,对实时软件可靠性的依赖正在以前所未有的速度增长,实时软件的可靠性设计与保障在实时系统中占据着越来越重要的位置,软件可靠性也成为了实时软件的一个重要指标。而传统的统一建模语言(United Modeling Language, UML)虽然被应用于软件的建模,但是却存在两个缺点。(1)其本身缺乏对于资源、时间等对于系统行为要求比较复杂的元素的相关描述,因而对于实时系统的软件建模存在不足;(2)缺乏精确的形式化语义定义,不能对于软件模型进行形式化验证和分析,因而难以确保软件的可靠性和安全性。针对这两点不足,要通过UML语言的扩展以及软件形式化描述来弥补。嵌入式实时系统建模与分析(Modeling and Analysis of Real Time and Embedded Systems, MARTE)是OMG组织在2009年提出的对于UML的profile,它弥补了UML在软件建模方面对时间、资源等非功能属性的匮乏。而形式化方法如petri网、进程代数、价格时间自动机则是对于软件的形式化描述语言,他们通过形式化的数学符号描述软件系统,使软件更精确,更可靠。模型驱动体系结构(Model Driven Architecture,MDA)是一种以模型为中心的软件开发框架,其本质是建模与模型转换。本文提出了一种基于MDA的实时软件资源建模与模型转换的方法。首先通过元建模抽象出包含资源信息的MARTE元模型以及价格时间自动机的元模型;然后利用模型转换语言ATL针对MARTE元模型和价格时间自动机元模型构造转换规则,通过将对应的实例模型进行相互转换,实现在MDA下MARTE模型到价格时间自动机模型的转换;最后通过形式化工具Uppaal Cora对模型转换结果进行形式化验证。实例分析表明该方法的可行性与有效性,它能够提高实时软件资源建模的可信性。本文先后探讨了:(1)如何通过元建模抽象出包含资源信息的MARTE元模型以及价格时间自动机的元模型。通过UML profile MARTE资源元建模以及与之同构化的价格时间自动机元建模。(2)如何利用模型转换语言ATL针对MARTE元模型和价格时间自动机元模型构造转换规则,通过将对应的实例模型进行相互转换,实现在MDA下MARTE模型到价格时间自动机模型的转换。(3)如何通过形式化工具Uppaal Cora对模型转换结果进行形式化验证。