（计算机应用技术专业论文）基于mde的uml模型到形式化模型的转换方法研究.pdf

n a n j i n gu n i v e r s i t yo f a e r o n a u t i c sa n da s t r o n a u t i c s n 圮g r a d u a t es c h o o l c o l l e g eo fi n f o r m a t i o ns c i e n c ea n dt e c h n o l o g y t h er e s e a r c ho nm o d e lt r a n s f o r m a t i o n b a s e do nm d ef o rr e a l - t i m e s y s t e m 跆r i f i c a t i o n a 砀e s i si n c o m p u t e rs c i e n c ea n dt e c h n o l o g ye n g i n e e r i n g b y l i u y a p i n g a d v i s e db y p r o f h u a n gz h i - - q i u s u b m i t t e di np a r t i a lf u l f i l l m e n t o ft h er e q u i r e m e n t s f o rt h ed e g r e eo f m a s t e ro f e n g i n e e r i n g d e c e m b e r , 2 0 0 9 承诺书 本人声明所呈交的博士学位论文是本人在导师指导下进 行的研究工作及取得的研究成果。除了文中特别加以标注和致 谢的地方外，论文中不包含其他人已经发表或撰写过的研究成 果，也不包含为获得南京航空航天大学或其他教育机构的学位 或证书而使用过的材料。 本人授权南京航空航天大学可以将学位论文的全部或部 分内容编入有关数据库进行检索，可以采用影印、缩印或扫描 等复制手段保存、汇编学位论文。 ( 保密的学位论文在解密后适用本承诺书) 作者签名：刹坠车 日 期：出每! 司啤一 南京航空航天大学硕上学位论文 摘要 实时系统的正确性不仅取决于计算的逻辑结果，而且依赖于系统运行的时间。如何确保实 时系统的正确性和可靠性是软件研究人员广泛关注的问题。u m l ( u n i t e dm o d e l i n gl a n g u a g e ) 是一 种通用的标准化的建模语言，适用于软件开发的各个阶段，但其缺乏精确的语义信息，因此难 以直接进行验证。而形式化方法( f o r m a lm e t h o d s ) 提供了一种严格精确的数学方法，通常被用于 软件设计阶段，分析系统的可靠性。因此，通过将u m l 模型转换到形式化模型进行模型验证， 是保证软件质量的有效手段。m a r t e ( m o d e l i n ga n da n a l y s i so f r e a lt i m ea n de m b e d d e ds y s t e m s ) 是o m g 组织专门针对嵌入式实时系统的建模规范，用于取代原有的u m l - s p t ( u r r dp r o f i l ef o r s c h e d u l a b i l i t y , p e r f o r m a n c ea n dt i m e ) 。时间自动机( t h et i m e da u t o m a t a ) 是一种成熟的实时系统模型 验证工具，它扩展了自动机理论，并为实时系统行为的创建和分析提供了一种形式化方法。 模型驱动工程( m o d e l - d r i v e ne n g i n e e r i n g ，简称m d e ) 的理念伴随着人们对软件系统的不断抽 象，而逐渐受到重视。它以模型为首要软件制品( s o l , w a r ea r t i f a c t ) ，其主要的研究方向为( 元) 建模和模型转换。元元模型体系( m e t a - m e t a m o d e la r c h i t e c t u r e ) 根据抽象度的不同，划分出元- 元 模型( m e t a - m e t a m o d e l ) 、元模型、模型( 和实例) 等三( 四) 个层次，其中抽象度低的模型遵从 抽象度高的元模型。元元模型是元模型的“根”，它为所有遵从它的元模型之间的桥接，提供 了一种共同的方式。本文给出了一种基于m d e 的u m l m a r t e 模型到时间自动机模型的转换 方法，它包含三个步骤：首先通过时间自动机的元建模，将其引入到m d e 的元元模型体系中； 然后，定义u m l m a r t e 和时间自动机元模型之间的映射规则，并由模型转换语言的支撑平台 实施转换过程；最后，按照模型检测工具的输入格式，将转换得到的时间自动机模型进行重写， 以便进行模型验证。 本文先后探讨了： 1 如何基于m d e ，将u m l m a r t e 模型转换到时间自动机验证模型。它关注两个方面： 1 ) 如何将时间自动机集成到元元模型体系；2 ) 如何实现基于元模型的模型转换。 2 通过对时间自动机元建模，将其集成到元- 元模型体系。集成的目的是为了让时间自动 机和i n 沮m a r t e 拥有共同的“根和操作集，从元模型层实现两者的相互理解。 3 通过定义元模型层的映射规则，实现i 脚m a r t e 模型到时间自动机模型的转换。转 换过程实际上是由映射规则定义语言的支持平台执行。由于模型检测工具通常由自己 的输入格式，因此，整个模型转换过程还附带了从模型到文本描述转换的过程。 关键字：模型驱动工程，模型验证，模型转换，u m i j m a r t e ，时间自动机 基于m d e 的u m l 模型到形式化模型的转换方法研究 a b s t r a c t h o wt oe n s u r et h es a f e t ya n dr e l i a b i l i t yo fr e a l - t i m es y s t e m s ，i nw h i c ht h ec o r r e c t n e s so ft h es y s t e m d e p e n d sn o to n l yo nt h el o g i c a lr e s u l t so fc o m p u t a t i o nb u ta l s oo nt h et i m ea tw h i c h t h er e s u l t sa r c p r o d u c e d , i sw i d e l yc o n c e r n e db y r e s e a r e h e r s t h eu m li sa w i d e l y - u s e ds t a n d a r dm o d e l i n gl a n g u a g e ， b u ti ti sd i f f i c u l t yt ob ea p p l i e df o rv e r i f i c a t i o nd i r e c t l y mf o r m a lm e t h o d ss u p p o r tf o r m a l v e r i f i c a t i o nb yt r a n s f e r i n gt h es y s t e mv e r i f i c a t i o np r o b l e mi n t oam a t h e m a t i c a lo n e t h e r e f o r e ，t h e m o d e lv e r i f i c a t i o n ，t h r o u g ht h et r a n s f o r m a t i o nf r o mu m lm o d e l st of o r m a lm o d e l s ，h a sb e c o m et h e h o t s p o ti nt h ef i e l do fs o f t w a r ee n g i n e e r i n g t h eu m lp r o f i l ef o rm o d e l i n ga n da n a l y s i so f r e a l - t i m ea n de m b e d d e ds y s t e m s ( m a r t e ) h a sb e e nr e c e n t l ys t a n d a r d i z e db yt h eo m gf o r r e a l - t i m es y s t e mm o d e l i n g mt i m e da u t o m a t ao a ) i sa ne f f e c t i v et o o lf o rt h ev e r i f i c a t i o no fm o d e l c h e c k i n g , w h i c hp r o v i d e saf o r m a lm e t h o dt oe s t a b l i s ha n da n a l y z e t h eb e h a v i o ro f r e a l - t i m es y s t e m s m o d e l - d r i v e ne n g i n e e r i n g ( m d e ) i san e wp a r a d i g mi ns o f t w a r ee n g i n e e r i n gw h i c ht r e a t sm o d e l s a st h ef i r s tc l a s sc i t i z e n s ，a n di m p l e m e n t ss o f t w a r eb y ( m e t a - ) m o d e l i n ga n dm o d e lt r a n s f o r m i n g t h e m e t a - m e t a m o d e li nm d ep r o v i d e sac o m m o nw a yo fb r i d g i n gt h o s em o d e l sc o n f o r m i n gt ot h es a n l e m e t a - m e t a m o d e l i nt h i sp a p e r , w ep r e s e u tam d e - b a s e da p p r o a c ht ob u i l db r i d g e sb e t w e e nm a r t e m o d e l sa n dt am o d e l sf o rv e r i f i c a t i o n i tc o n s i s t so ft h r e es t e p s ：t h ef i r s ts t e pi st h em e t a m o d e l i n go f t a ，w h i c hb r i n g st ai n t om e t a - m e t a m o d e la r c h i t e c t u r ei nm d e ；t h es e c o n di sd e f i n i n gm a p p i n gr u l e s b e t w e e nm e t a m o d e l so fm a r t ea n dt a ，a n di ti si m p l e m e n t e db yt h ep l a t f o r mi ns u p p o r to f t r a n s f o r m a t i o nl a n g u a g e s ；t h en l i r di st or e w r i t et am o d e l si n t ot e x t u a li n p u t so fm o d e lc h e c k i n gt o o l s f o rv e r i f i c a t i o n 硼1 em a i nc o n t r i b u t i o n so ft h i st h e s i sa r ea sf o l l o w s ： 1 t h em d e - b a s e da p p r o a c ht ot r a n s f o r mm a r t em o d e l si n t ot am o d e l sf o rv e r i f i c a t i o ni s p m s e n t e d i tf o c u s e so nt w oa s p e c t s ：t h eh e t e r o g e n e o u sm o d e l si n t e g r a t i o nb ym e t a m o d e l i n g a n dt h em o d e lt r a n s f o r m a t i o nb a s e do nm e t a m o d e l s 2 t h em e t a m o d e lo ft ai sb u i l d e df o ri n t e g r a t i n gt ai n t om e t a - m e t a m o d e la r c h i t e c t u r e i ti s i n t e n d e dt oe n s u r et h a tt h em e t a m o d e lo ft ah a st h es 锄e “r o o t a sm a r t e ，s ot h e yc a nh a v e t h es a m eo p e r a t i o ns e t s 3 t h em o d e lt r a n s f o r m a t i o nb a s e do nm d ei si m p l e m e n t e db yd e f i n i n gt r a n s f o r m a t i o nr o l e s b e t w e e nm e t a r n o d e l s b e c a u s em o s to fm o d e lc h e c k i n gt o o l sd e f i n et h e i ro w nt e x t u a li n p u t f o r m a t s ，h e n c et h e r ei s 觚a d d i t i o n a lp r o c e s sb r i n g i n gm o d e l si n t ot e x t u a ld e s c r i p t i o n s k e y w o r d s ：m o d e l - d r i v e ne n g i n e e r i n g ，m o d e lv e r i f i c a t i o n , m o d e lt r a n s f o r m a t i o n ，m a r t e t i m e d a u t o m a t a i l 南京航空航天大学硕士学位论文 目录 第一章绪论l 1 1 课题研究背景1 1 2 研究现状及选题依据。2 1 2 1 国内外研究现状2 1 2 2 选题依据3 1 3 论文主要工作及组织结构。4 第二章基于m d e 的模型转换框架5 2 1 模型驱动工程( m d e ) 5 2 1 1 模型驱动体系结构。6 2 1 2 领域特定语言7 2 1 3m d e 实现平台和工具8 2 2 模型和模型转换9 2 2 1 模型与元模型9 2 2 2 纵向模型转换1 0 2 2 3 横向模型转换1 l 2 3 面向验证的模型转换方法1 2 2 3 1 模型转换过程1 2 2 3 2 模型转换实现途径1 3 2 4 本章小结1 4 第三章实时系统建模语言的元模型1 5 3 1u m l 实时扩展0 v u a 艾t e ) 的元模型。1 5 3 1 1 时间相关的建模元素1 6 3 1 2 系统设计建模元素1 7 3 2 时间自动机的元模型1 8 3 2 1 时间自动机的语法和语义1 8 3 2 2 时间自动机的类型结构2 0 3 3m a r t e 和时间自动机元模型问的同构化。2 2 3 3 1 同构化的实现方法2 2 3 3 2 与m a r t e 同构的时间自动机元模型2 3 i i i 基于m d e 的u m l 模型到形式化模型的转换方法研究 3 4 本章小结2 7 第四章m a r t e 模型到时间自动机模型的转换2 8 4 1 模型转换的内容2 8 4 1 1 模型转换的实施原理2 8 4 1 2 模型转换实施过程3 0 4 2 元模型间的映射关系3 0 4 2 1 类型结构的映射规则3 l 4 2 2 行为的映射规则3 2 4 3 模型到文本的相互转换3 6 4 3 1 模型到文本的转换3 6 4 3 2 文本到模型的转换3 8 4 4 本章小结3 8 第五章模型转换的应用4 0 5 1 实时系统问题描述4 0 5 2 采用m a r t e 的系统建模4 0 5 3m a r t e 到时间自动机的模型转换。4 2 5 4 验证的输入模型生成4 7 5 5 模型检测与分析4 9 5 5 1 模型检测4 9 5 5 2 检测结果分析与讨论5 0 5 6 本章小结5 2 第六章总结与展望5 3 6 1 论文总结5 3 6 2 今后工作5 4 i v 南京航空航天大学硕士学位论文 图表清单 图1 1q v t 语言架构。3 图2 1m d e 原则、标准和工具5 图2 2 三层元元模型体系。1 0 图2 3m d a 中主要的模型转换1 0 图2 4 异构模型转换框架1 2 图2 5 元元模型体系下u m l 模型和形式化模型之间的转换过程1 3 图2 6 基于a m m a 的异构模型转换框架1 4 图3 1m a r t e 包结构图1 6 图3 2m a r t e 时间相关的设计元素1 7 图3 3m a r t e 设计元素18 图3 4k m 3 元元模型2 2 图3 5 对时间自动机数据类型元建模2 3 图3 6 对时间自动机函数、变量、表达式的元建模2 4 图3 7 对时间自动机组成结构的元建模2 5 图4 1a t l 遵循的模型转换视图2 8 图4 21 s 应用视图2 9 图4 3 模型转换实施过程3 0 图4 4u m l 状态机视图元素3 3 图4 5u m l 活动视图元素3 4 图4 6 眦交互视图元素。3 5 图5 1t r a i ng a t e 系统类图设计4 0 图5 2t r a i ng a t e 系统动态视图设计4 2 图5 3 实施a t l 转换的配置视图4 3 图5 4t r a i ng a t e 系统模型转换的结果4 8 图5 5t r a i ng a t e 系统分析- g a t e 对象的修改5 1 表4 1 状态机图和时间自动机元素之间的映射关系3 3 表4 2 活动图和时间自动机元素之间的映射关系3 4 表4 3 交互视图到时间自动机元素之间的映射关系3 5 表5 1 对t r a i n _ g a t e 系统进行模型检测的检测规则和结果4 9 v 基于m d e 的u m l 模型到形式化模型的转换方法研究 注释表 m d e ( m o d e ld r i v e ne n g i n e e r m 卜模型驱动工程：一种软件开发方法，它以模型为首要软 件制品，通过建模为问题域构造软件系统的业务模型，然后依靠模型转换驱动软件开发，( 半) 自动地产生最终完备的应用程序。 m d a ( m o d e ld r i v e na r c h i t e c t ur e _ 卜_ 模型驱动框架：是国际标准化组织o m g 于2 0 0 1 年提出 的一种基于模型的软件开发框架性标准，它是最具代表性的m d e 实现框架。 m o f ( m e t ao b j e c tf a c h i 衄卜一是o m g 提出的一种对元模型进行描述的规范的公共抽象定义 语言。它是一种元元模型，即元模型的元模型。 u m l ( u n i t e dm o d e l i n gl a n g u a g e 卜一统一建模语言：是一种为离散系统建模的图形语言，它 可以在抽象级对软件系统及其用途进行明确的、可视化的详细描述、构造和只是归档。 m a r t e ( m o d e l i n ga n da n a l y s i so fr e a lt i m ea n de m b e d d e ds y s t e m s 卜是o m g 组织专门 针对嵌入式实时系统的建模规范，用于取代原有的u m l - s p t ( u m l p r o f f i ef o rs c h e d u l a b i l i t y , p e r f o r m a n c ea n dt i m e ) 。 时间自动机( t i m e da u t o m a t 心一一种成熟的实时系统模型验证工具，它扩展了自动机理论，并 为实时系统行为的创建和分析提供了一种形式化方法。 u p p a a i 广一是一个对实时系统建模、模拟和验证的工具箱，最早发布于1 9 9 5 年，此后一直由 u p p s a l a 大学和a a l b o r g 大学协作维护开发。 d s l ( d o m a i ns p e c i f i cl a n g u a g 介_ 域特定语言：它是一种特化的，面向问题的语言。 a m m a ( a t l a s m o d e l m a n a g e m e n t a r e h i t e e t u 弛卜一是一个模型管理平台，支持( 元) 建模、 模型转换、模型编织和模型管理。它建立在基于模型的d s l 的基础上，提供了一套核心d s l s 。 q v t ( q u e r y v i e w t r a n s f o r m a t i o n 卜一是o m g 为实现模型自动转换，而提出的基于m o f 模 型的相互转换的标准。 a t l ( a t l a st r a n s f o r m a t i o nl a n g u a g 竹一是a t l a si n r i a l i n a 研究组织针对o m gm o f q v tr f p 的解决方案。它是一种说明式( d e c l a r a t i v e ) a 和命令式( i r r l p e m d v e ) 混合的编程语言，使 用o c l 作为约束语言。 圈m 3 ( k e r n e lm e t a m e t a m o d e i 卜是一种轻量级的文本元模型定义语言，它有清晰的语义，并 且使得元模型的创建和修改变得容易。 t c s ( t e x t u a lc o n c r e t es y n t a x _ 卜琨a m m a 平台中独特的组成部分，它专门为沟通模型域与 文本域而设计，最早设计思路来源于o m g 的m o f 模型到文本转换语言提案需求，目前已成 为e c l i p s e 下的开源项目。 a m w ( a t l a s m o d e lw e a v e 什一是a m m a 平台下建立模型之间关系的工具，它将模型之间 的联系保持在编织模型中，基于m d a 的架构，该编织模型也遵循模型编织元模型。 m t f ( m o d e lt r a n s f o r m a t i o nf r a m e w o r 埘一是i b m 开发的一个模型转换工具，主要用来在 模型之间进行转换，可以讲代码看成一种模型，所以m t f 也可以用于一些代码的生成。 v i 南京航空航天大学硕士学位论文 第一章绪论 1 1 课题研究背景 目前，嵌入式实时系统已广泛应用于工业控制、通信、航空航天等领域。与传统的非实时 系统相比，嵌入式实时系统有更强的时间约束，对可靠性、可预测性也有更高的要求。因此， 嵌入式实时系统的设计也呈现不同的特性，需要良好的方法、工具和语言的支持。u m l 1 】是一 种通用的，有工具支持的标准化建模语言，强调建模的灵活性和实用性，支持对系统静态和动 态的多个侧面进行建模，得到工业界的广泛认同。但它是一种半形式化建模语言，缺乏精确的 语义，难以直接进行形式化分析与验证，以满足实时系统高可靠性需求。而形式化方法作为一 种以数学为基础的方法，能够清晰、精确、抽象、简明地规范和验证软件系统及其性质，极大 地提高软件的安全性和可靠性。因此，需要将u m l 模型转换到形式化模型进行验证，以保证 软件的可信度。 伴随着信息化进程的迅猛发展，软件系统日益复杂。一方面，计算环境的演变，开放化、 互联化、标准化、组件化已经成为软件的根本要求；另一方面，i n t e m e t 的诞生和普及，极大改 变人类社会生活方式的同时，也使软件系统呈现出新的异构性、动态性等特点。传统的以代码 为中心的软件开发方法面临着各种问题：1 ) 软件设计与实现脱节；2 ) 不同平台、不同技术路 线之间的集成和互操作问题；3 ) 新技术和新平台与现有软件的集成问题。系统建模是软件开发 史上的一次革命，模型是对软件系统的一种抽象。它是指从众多的软件系统中抽取出共同的、 本质性的特征，而舍弃其非本质的特征。在这种背景下，软件驱动工程逐渐受到重视，它被认 为是应对“高效、低成本地开发优质软件一 2 1 的有效途径。 模型驱动工程 2 1 以模型为首要软件制品，通过对问题域建模构造软件系统的业务模型，然后 依靠模型转换驱动软件开发，( 半) 自动地产生最终完备的应用程序 2 1 。m d e 下一系列工作都 围绕模型展开，r o b e r tf r a n c e 3 将这些工作中最重要和亟待解决的问题归为如下几类挑战： 1 建模语言的挑战：它主要来自于如何使建模语言支持在问题层面上进行建模，以及如 何对模型进行严格的分析。 2 关注点划分的挑战：它来源于对同一系统进行多视图建模的结果。由于不同侧面的模 型可能是基于异构的语言开发的，而模型间又存在着相互重叠的部分，因而很容易出 现不一致等问题。 3 对模型的操纵和管理的挑战：它包括了1 ) 对模型转换的定义、分析和使用；2 ) 维护 模型元素间的可追溯性。以支持模型演化和双向工程；3 ) 维护不同视点之间的一致性： 4 ) 版本追踪；5 ) 在运行期使用模型。 基于m d e 的u m l 模型到形式化模型的转换方法研究 前两类是针对建模，最后一类主要是转换的问题。在建模方面，如何高效地构造模型一直 是m d e 中的一个研究热点。从语言层面上来考虑这个问题的解决方法不失为一个好的思路。 目前，建模技术发展的结果是出现了众多的建模语言，并导致大量异构模型的出现。它们被广 泛应用在不同领域中，却难以彼此复用和交互。众多的异构模型的存在，在进一步推动建模语 言本身发展的同时，为模型的可复用性和可移植性带来问题。模型转换，可以说是模型驱动思 想在发挥实质性作用【4 】。它可以发生在不同抽象层之间( 从高到低的正向工程，或从低到高的逆 向工程) 和同一抽象层之间( 异构模型集成) 。模型的异构性是由于建模语言的异构性造成的，而 解决异构建模语言之间交互障碍的一个直接而有效的方式就是将异构模型转化为同构模型加以 集成。 传统的异构模型转换大多数是a d - h o c 式的，即针对特定的异构模型建立专门的转换。它不 仅导致大量的重复，不利于模型转换规则的重用，且在为原有模型增加新的语言成分时，需要 重新构建原来的转换关系。而在m d e 框架下，通过遵循共同的元语言，有效提高了模型转换 的独立性和有效性【5 】。 1 2 研究现状及选题依据 1 2 1 国内外研究现状 模型驱动框架( m o d e ld r i v e na r c h i t e c t u r e ，简称m d a ) 网是国际标准化组织o m g 于2 0 0 1 年提出的一种基于模型的软件开发框架性标准，它是最具代表性的m d e 实现框架。m d a 是一 种提倡业务逻辑与实现技术分离的软件开发方法。张天【5 】等人通过研究一个具有代表性m a r t e 到f i a c r e 模型的转换实例，探讨了异构模型之间在语义和语法层的相互转换问题：在语义层， 通过模型转换技术构造语义映射规则，实现元语言之间的转换；在语法层，通过构造元模型的 具体语法，反映元语言的语法规则，从而产生目标模型的程序实体。 m d a 中需要解决的两个主要问题是如何有效地建立软件模型以及如何在模型之间进行有 效的转换。前者目前已经达成了较为一致的意见，即以u m l 及其扩展机制作为建模的标准语 言；后者目前仍然没有一个统一的答案。模型转换是模型驱动架构中的核心技术，其目的是为 了解决软件开发过程中以模型作为基础元素的查询、变换、视图等技术问题。o m g 组织于2 0 0 2 年提出了q v t ( q u e r y v i e w t r a n s f o r m a t i o n ) r f p ，寻求统一的模型转换标准，共收到8 个q v t 提案，经过几年的反馈和演变，最终于2 0 0 5 年底形成一个统一的提案，并审批通过【7 1 。 q v t 定义了一种将源模型转换为目标模型的标准方式，如下图示：q v t 定义了三种领域特 定语言：r e l a t i o n s 、c o r e 和o p e r a t i o n a lm a p p i n g ，它们被组织在一个分层架构中。r e l a t i o n s 和 c o r e 是在两种抽象层次上的声明式语言，它们之间有规范性映射。o p e r a t i o n a lm a p p i n g 语言是 r e l a t i o n s 和c o r e 的扩展，它是一种命令式语言。b l a c kb o x 机制是用来调用其他语言描述的转 2 南京航空航天大学硕士学位论文 换设施，它也是q v t 规范的重要组成部分，可用于集成现有的非q v t 库。 r e l a t i o 嬲 | 卜 - 趸r e l a t i o n s 墨田 喜甚 t oc o r e 昂胃 翼量! 竺竺吵 暑粤 v 曼晏 口 一 c 。托 卜 图1 1q v t 语言架构 目前尚没有与q v t 完全兼容的模型转换语言，开源社区创建了一种实用的解决方案。a t l a s t r a n s f o r m a t i o nl a n g u a g e ( a t l ) 闱提供非常类似q v t 的解决方案：它包含自己的编译器，编译器 产生包含基本转换操作的中间代码，具体由其虚拟机执行。这与q v t 的r e l a t i o n s 翻译成 o p e r a t i o n 执行类似。a t l 使用的概念也与q v t 类似，遵从的元一元模型体系，而且转换语言支 持o c l 的子集。 m d a 着重于两个关键的概念：模型与模型转换，它能桥接设计建模概念与分析特定的概念， 用于软件建模与分析：o m g 指定o c l 描述u m l 模型的约束，但软件工程并不只有u m l ，领 域特定语言o 艇i i i ls p e c i f i cl a n g u a g e ，简称d s l ) 9 促进大量特定领域的元模型，而当前d s l 工具很少能评价模型的约束，j e a nb 6 z i v i n 等【1 0 1 演示了如何使用a t l 来检查模型的约束。 a b d e l o u a h e dg h e r b i 等【1 1 1 通过对a t l 定义元模型之间的映射，将实时系统的u m l 模型转换到 调度模型。 1 2 2 选题依据 实时系统要求系统不仅要满足逻辑约束，还要满足时间约束，它对可靠性、安全性等有更 高地要求。u m l 强调建模的灵活性和实用性，但缺乏精确地语义，难以满足实时系统高可靠性 的要求。因此，需要将u m l 模型转换到形式化模型进行验证，提高软件的可信度。传统的从 u m l 到形式化模型的转换，多是a d - h o c 式，转换关系和转换规则难以重用。如t a b u c h i ，n 等 人将遵从u m l - s p t 的状态图和活动图转换到随机进程代数1 2 j ；m i r c ot r i b a s t o n e 等从u m l 活动 图抽取p e p a 模型【1 3 1 。 模型转换是m d e 中是最重要的部分，q v t 是o m g 组织定义的模型转换标准，旨在定义 特定领域的语言来查询、查看并转换模型。o m g 倡导的元元模型体系为模型转换注入新的思 路，即通过统一的元一元模型设计各种领域建模语言，从元模型的层次上消除异构性，并提高转 3 基于m d e 的u m l 模型到形式化模型的转换方法研究 换的独立性和灵活性。法国i n r i a 的a t l a s 研究组提出的a m m a ( a t l a sm o d e lm a n a g e m e n t a r c h i t e c t u r e ) 平台【1 4 】，为高效、实用地建立这样的转换桥，提供了有力的支持。a t l 正是 a t l a s ( i n r i a & l i n a ) 对q v tr t f 的解决方案，它是一种指定元模型和文本具体语法的模型转 换语言，为开发者架起依照指定方式从源模型集合产生目标模型的桥梁，目前已在a m m a 平 台下实现。 基于a t l 的模型转换有以下优点【5 l ：1 转换维护，模型转换可能随时间演变，而a t l 的转 换规则结构更容易理解和维护；2 可追溯性，a t l 存储源模型与目标模型元素之间的映射关系， 它支持模型转换过程的跟踪；3 工具支持，a t l 有a m m a 平台的支持，只需定义源模型与目 标模型元素映射关系，即可实施转换过程。 1 3 论文主要工作及组织结构 本文研究了基于m d e 的实时系统u m l 模型到形式化模型的模型转换。对实时系统进行模 型验证是本文的目的，从u m l 设计模型到形式化模型的模型转换是本文的实现手段，而m d e 是本文使用的方法。本文的主要工作在于：1 ) 给出了一种基于m d e 的面向验证的模型转换方 法：2 ) 通过对形式化模型进行元建模，完成了u m l 和形式化模型的同构：3 ) 通过定义元模 型层之间的映射规则和模型的文本语法规则，实现了u m l 模型到时间自动机模型的转换。围 绕主要工作，本文的内容结构作如下安排： 第一章阐明课题的研究背景，介绍和分析课题的研究现状和选题依据，并概述本文的主要 研究工作。 第二章对m d e 的实现框架和实现平台简要介绍后，针对m d e 的两个主要研究内容：模型 和模型转换进行论述，最后定义本文的模型转换过程并给出实现途径。 第三章对u m l 实时建模规范m a r t e 和时间自动机的元模型进行研究和分析，讨论了 m a r i e 和时间自动机同构的方法，并通过对时间自动机元建模实现异构模型的同构。 第四章给出m a r t e 模型到时间自动机模型的模型转换具体过程及实现方法后，从类型结 构和行为两方面对元模型间的映射关系进行分析，最后通过定义文本具体语法，讨论模型和文 本间的相互转换。 第五章结合具体的实时系统案例，完成从系统建模、模型转换、文本转换、检测分析这一 系列过程，它是对第四章元模型问映射规则和模型的文本具体语法的具体应用。 第六章总结全文，分析本文的主要贡献并对未来工作做进一步展望。 4 南京航空航天大学硕士学位论文 第二章基于m d e 的模型转换框架 在软件开发的长期摸索过程中，人们逐渐认识到有效地利用抽象，是解决软件开发问题的 具体而实用的途径。过去五十年以来，软件研究者和开发人员创建了一系列抽象以帮助他们就 设计意图编程，而从复杂的编程环境中解脱出来【2 】。同时，伴随着信息化进程的迅猛发展，软 件的复杂度也在不断提高，软件的演进形态也日益多样化。在这种情况下，如何缓解复杂性， 有效地表述领域概念成为学术和工业界共同关注的焦点。模型驱动工程在此背景下逐渐收到重 视，它被认为是解决上述问题的有效途径，而这一认识也正伴随着实践不断得到深化。 2 1 模型驱动工程( m d e ) 最早支持m d e 的工具是上世纪八十年代的c a s e ( c o m p u t e r - a i d e ds o f t w a r ee n g i n e e r i n g ) 1 6 1 ， 它致力于开发一套软件方法和工具，来帮助软件开发者用图例( 如状态机图、结构图和数据流 图等) 表述其设计意图，以减少人工编码、调试。然而，由于平台的复杂性和自身的局限性， c a s e 的应用被局限于研究和商业文献中【2 】。为了应付复杂而且不断演变的软件问题的解决方 案，m d e 仍在不断演化。尽管尚未研究出稳定而健全的基础