（计算机软件与理论专业论文）嵌入式基于模型驱动验证及软件生产线的研究与实现.pdf

西南交通大学硕士研究生学位论文第1 页 摘要 随着处理器的计算能力的迅速提高、嵌入式技术的迅猛发展和嵌入式系统应用领域 的不断拓宽，使得嵌入式软件的规模以及复杂性的不断增长，从而导致了开发时间和 费用也在不断的增长，如何快速有效的开发嵌入式软件成为目前亟待解决的问题。为 了解决上面的问题，全球最大的软件工业标准化组织o m g ( o b j e c t m a n a g e m e n tg r o u p ) 提出了模型驱动框架m d a ( m o d e ld r i v e na r c h i t e c t u r e ) 开发方法。m d a 方法将软件 开发过程分成两个主要阶段：模型级和代码级。模型主要关注系统的设计正确性，从 而达到以较小代价修改软件错误的目的。 面向嵌入式软件的开发工具目前正在从基于代码的传统开发环境向基于模型的开 发环境发展。而一个基于模型的嵌入式生产线开发环境，应该是集成模型开发工具和 其他相关工具，包含了建模、模型仿真验证、代码生成、测试等嵌入式软件开发的全 过程。这符合嵌入式软件开发工具发展趋势，也具备相应的理论、技术和产品基础。 模型驱动验证是基于模型的嵌入式软件生产线的一个重要部分，这个关键部分会影 响到系统的质量和后期的工作，如果在前期能够及时发现出存在的问题，可以节省大 量的人力物力。当今主流的嵌入式实时系统中，实时性是一个关键的性能指标，对于 这类系统就是要求它们在合法的时间内完成相应的行为，不会发生超时现象，这就要 求验证任务间的可调度性来判断系统实时性是否符合要求。由c l a r k 和e m e r s o n 提出形 式化的模型验证的方法以开始应用在任务的可调度分析上，该方法的基本原理是为要 检测的系统建立形式化模型，阐明所要验证的性质，然后使用算法去检查该模型是否 满足所述性质。 本文的研究是基于模型的软件嵌入式生产线开发环境，在这条主线上把重点放在研 究和解决模型方面的形式化验证问题，对嵌入式模型实时性中的可调度问题进行研究。 论文先介绍了基于模型的嵌入式软件生产线的背景与意义，并分析了国内外的发展 情况，接着说明课题的来源和本文研究的内容；在此基础上提出基于模型的嵌入式生 成线的总体需求分析；接着重点介绍模型验证调度检测工具s c t ( s c h e d u l i n gc h e c k t 0 0 1 ) 的设计，包括s c t 所分析的系统的相关定义和规定以及任务的两个行为自动机 模型的设计实现，在这些前提下对s c t 工具进行总体设计，并对每部分进行实现，其 中重点放在调度仿真算法进行设计与实现；接着在l a m b d a p r o 的基础上集成相关工 具，实现基于模型的嵌入式软件生成线的整个开发过程，并通过一个实例应用来说明 验证这个开发流程。论文最后对本文的工作进行总结，并对后继研究和发展进行了展 望。 关键字：模型驱动；嵌入式软件生产线；模型仿真验证；可调度性；s c t ；集成 西南交通大学硕士研究生学位论文第| | 页 a b s t r a c t t h es i z ea n dc o m p l e x i t yo ft h ee m b e d d e ds o f t w a r eg r o wc o n s t a n t l y ，f o rt h er e a s o nt h a t t h er a p i di m p r o v e m e n to ft h ec o m p u t i n gp o w e ro fp r o c e s s o r s ，t h er a p i dd e v e l o p m e n to f e m b e d d e dt e c h n o l o g y ，a n dt h ec o n t i n u o u s l ye x p a n d i n go ft h ef i e l do fe m b e d d e ds y s t e m a p p l i c a t i o n s ，w h i c hr e s u l t si ni n c r e a s i n gt i m ea n dc o s t so nd e v e l o p m e n t t h e r e f o r e ，h o wt o d e v e l o pe m b e d d e ds o f t w a r ef a s ta n de f f e c t i v e l yb e c o m eas e r i o u sp r o b l e m t h ew o r l d s l a r g e s ts o f t w a r ei n d u s t r y s t a n d a r d s o r g a n i z a t i o no m g ( o b j e c t m a n a g e m e n tg r o u p ) p r o p o s e d am o d e l - d r i v e nf r a m e w o r km d a ( m o d e ld r i v e n a r c h i t e c t u r e ) d e v e l o p m e n t m e t h o d o l o g yi no r d e rt os o l v et h ea b o v ep r o b l e m s m d am e t h o d o l o g yd i v i d e ss o f t w a r e d e v e l o p m e n tp r o c e s si n t ot w om a i np h a s e s ：m o d e l l e v e la n dc o d el e v e l m o d e li sm a i n l y r e s p o n s i b l ef o rt h ec o r r e c t n e s so fs y s t e md e s i g n , s ot h a to n l yl i t t l ec o s tw i l lb en e e d e dt of i x a ne r r o ri ne x i s t i n gs o f t w a r e r e c e n t l y ，t o o l sf o rd e v e l o p i n ge m b e d d e d - o r i e n t e ds o f t w a r ea r et r a n s f e r r i n gf r o mt h e t r a d i t i o n a lc o d e b a s e dd e v e l o p m e n te n v i r o n m e n tt om o d e l - b a s e dd e v e l o p m e n te n v i r o n m e n t am o d e l - b a s e de m b e d d e ds o f t w a r e p r o d u c t i o n l i n es h o u l d i n t e g r a t e m o d e lb a s e d d e v e l o p m e n tt o o l sa n do t h e rc o r r e l a t i v et o o l s ，a n dh e n c e ，i tc o v e r st h ee n t i r ed e v e l o p m e n t p r o c e s so fe m b e d d e ds o f t w a r e ，s u c ha sm o d e l i n g ，s i m u l a t i o n ，v e r i f i c a t i o n ，c o d eg e n e r a t i o n a n dt e s t i n g i ti sn o to n l yi nl i n ew i t ht h et r e n do fe m b e d d e ds o f t w a r et o o l s ，b u ta l s oh a st h e c o r r e s p o n d i n gt h e o r e t i c a l ，t e c h n i q u e ，a n dp r o d u c tf o u n d a t i o n s m o d e l - d r i v e nv e r i f i c a t i o ni sa ni m p o r t a n tp a r to ft h em o d e l - b a s e de m b e d d e ds o f t w a r e p r o d u c tl i n e ，s ot h ek e yp a r tw i l lh a v ei m p a c to nt h eq u a l i t yo f t h es y s t e ma n dl a t e rw o r k i f e x i s t i n gp r o b l e m sc a nb ed e t e c t e di ne a r l i e rp h a s e ，i tc a ns a v eal o to fm a n p o w e ra n d r e s o u r c e s r e a l - t i m ep e r f o r m a n c ei sak e yi n d i c a t o ro ft o d a y sm a i n s t r e a me m b e d d e d r e a l t i m es y s t e m s ，w h i c hr e q u i r e sc o r r e s p o n d i n ga c t i o nt ob ec o m p l e t e di nt h el e g i t i m a t e t i m e ，a n dn oo v e r t i m ep h e n o m e n o n t h e r e f o r e ，i ti sn e c e s s a r yt ov e r i f yt h es c h e d u l a b i l i t y a m o n gt h et a s k st od e t e r m i n ew h e t h e rt h er e a l - t i m ep e r f o r m a n c eo fs y s t e m sm e e tt h e r e q u i r e m e n t s t h i sf o r m a l i z e dm o d e lv a l i d a t i o nm e t h o dw a sf i r s t l yp r o p o s e db yt h ec l a r k a n de m e r s o n ，t h eb a s i cp r i n c i p l ei st ot e s tt h es y s t e mf o re s t a b l i s h i n gf o r m a lm o d e l ，c l a r i f y t h en a t u r et ob ev e r i f i e d ，a n dt h e nu s et h ea l g o r i t h mt oc h e c kw h e t h e rt h em o d e lm e e t st h e r e q u i r e m e n t so rn o t b a s e do nd e v e l o p m e n te n v i r o n m e n to fm o d e le m b e d d e ds o f t w a r ep r o d u c tl i n e ，t h i s p a p e rw i l lp u tf o c u so nr e s e a r c ha n ds o l v et h ef o r m a lv e r i f i c a t i o np r o b l e m so fm o d e l so nt h e b a s i so fi t , a n ds t u d yt h es c h e d u l i n gp r o b l e mo fr e a l - t i m ee m b e d d e dm o d e l 西南交通大学硕士研究生学位论文第| l 页 f i r s t l y ，t h i sp a p e rw i l li n t r o d u c eb a c k g r o u n da n ds i g n i f i c a n c eo ft h em o d e l - b a s e d e m b e d d e ds o f t w a r ep r o d u c tl i n e ，a n a l y z et h ec u r r e n tt r e n d s ，a n dt h e ni l l u s t r a t et h es o l i c eo f t h es u b j e c to ft h i sp a p e ra n dt h ec o n t e n t so ft h i sp a p e r o nt h i sb a s i s ，t h ew r i t e rw i l lp r e s e n t a no v e r a l ln e e d sa n a l y s i so ft h em o d e l b a s e de m b e d d e ds o f t w a r ep r o d u c tl i n e i nt h e f o l l o w i n gp a r t ，t h ew r i t e rw i l lf o c u so ni n t r o d u c i n gt h ed e s i g no fs c ts c h e d u l i n gc h e c kt o o l s ， i n c l u d i n gt h er e l e v a n td e f i n i t i o n sa n dr u l eo ft h es y s t e ma n a l y z e db ys c t ，a n dd e s i g n i n ga n d i m p l e m e n t i n gt h et w ob e h a v i o r a la u t o m a t am o d e lo ft a s k s u n d e rt h ep r e m i s e ，t h ew r i t e rw i l l d e s i g na n di m p l e m e n tt h es c h e d u l i n g a n ds i m u l a t i o n a l g o r i t h mo fs c t b a s e d o i l l a m b d a p r o ，t h i sp a p e rw i l li n t e g r a t eo t h e rc o r r e l a t i v et o o l s ，a c h i e v et h ee n t i r ed e v e l o p m e n t p r o c e s so fm o d e l - b a s e de m b e d d e ds o f t w a r ep r o d u c tl i n e ，a n du s ea ne x a m p l ea p p l i c a t i o nt o i l l u s t r a t ea n dv a l i d a t et h i sd e v e l o p m e n tp r o c e s s f i n a l l y ，b ys u m m a r i z i n gt h es t u d yo ft h e p a p e r ，t h ea u t h o rg i v e sp r o s p e c to ff u t u r er e s e a r c ha n dd e v e l o p m e n t k e y w o r d s ：m o d e l - d r i v e n ；e m b e d d e ds o f t w a r ep r o d u c t i o nl i n e ；s i m u l a t i o na n dv e r i f i c a t i o n o fm o d e l ；s c h e d u l a b i l i t y ；s c t ；i n t e g r a t e 西南交通大学曲南父遮大字 学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、使用学位论文的规定，同意学校保留 并向国家有关部门或机构送交论文的复印件和电子版，允许论文被查阅和借阅。本 人授权西南交通大学可以将本论文的全部或部分内容编入有关数据库进行检索，可 以采用影印、缩印或扫描等复印手段保存和汇编本学位论文。 本学位论文属于 1 保密口，在 年解密后适用本授权书； 2 不保密使用本授权书。 ( 请在以上方框内打“、”) 学位论文作者签名：1 谚c 夕撼 指导老师签 日期：力oi o 2 1日期：7 0 细6 z 西南交通大学硕士学位论文主要工作( 贡献) 声明 本人在学位论文中所做的主要工作或贡献如下： ( 1 ) 深入研究e c l i p s e 框架结构，熟练掌握e c l i p s e 的插件开发技术。对基于 e c l i s p e 框架的l a m b d a p r o 集成开发环境的研究。对基于模型的嵌入式 生产线的需求进行设计分析，分析所需要集成的第三方软件，比如： t - v e c 、m a t l a b 、s i m u l i n k 等。 ( 2 )对基于模型的嵌入式生产线开发环境的整体框架的设计，并把第三方的 软件集成在l a m b d a p r o 上形成基于模型开发的一条生产线，包括把 o s a t e 系统框架模型开发工具、s i m u l i n k 功能模型开发工具、t - v e c 测 试用例生成工具等集成到l a m b d a p r o 上，使所有操作都在同一个开发 环境进行，并对框架代码跟功能代码合成实现。 ( 3 )在基于模型的嵌入式生产线中，对系统模型的非功能属性的验证是一个 重要的部分，尤其是系统的实时性验证，通过分析系统的调度性来衡量 系统的实时性。而形式化的调度分析验证可以提高系统的可靠性要求。 因此，要深入学习形式化验证的理论，如时间自动机理论和可达性理论。 ( 4 ) 在北京科银京成成都研发中心跟项目组同事一起研究开发调度检测工具 s c t ，设计s c t 所分析的系统、任务的行为自动机结构及调度仿真分析 算法。本入主要工作对调度仿真器，及其分析算法的设计与实现。 本人郑重声明：所呈交的学位论文，是在导师指导下独立进行研究工作所得的成 果。除文中已经注明引用的内容外，本论文不包含任何其他个人或集体已经发表或撰 写过的研究成果。对本文的研究做出贡献的个人和集体，均已在文中作了明确说明。 本人完全了解违反上述声明所引起的一切法律责任将由本人承担。 学位论文作者签名：够! 瑁鸭 日期：7 口fd 6 艺 西南交通大学硕士研究生学位论文第1 页 1 1 背景及意义 第1 章绪论 随着嵌入式处理器的计算能力的快速提高、集成电路技术的集成度越来越复杂， 以及嵌入式的应用领域越来越广泛，导致了嵌入式软件的规模以及复杂性的不断增长， 从而导致了开发时间和费用也在不断的增长，如何快速有效的开发嵌入式软件成为目 前亟待解决的问题。 在传统的嵌入式软件开发过程中，大多数是依靠编程人员手工编程技巧，虽然单 个功能模块的编写相对容易实现，但是在系统集成后如何满足整个系统的非功能属性 对于开发人员是一个巨大的挑战【l 】。嵌入式系统的功能和复杂度的提高，在更高的抽象 层次上进行系统级设计和软硬件协同设计的方法已经成为研究的热点。设计安全关键 的嵌入式系统要求充分捕获设计需求并快速构造满足系统功能属性和非功能属性。因 此形成一种快速建模和验证的设计方法非常重要。软件工程方法所提出的模型驱动结 构( m o d e l d r i v e na r c h i t e c t u r e ) 1 2 】通过实践证明是一种较有效的解决方法。m d a 方法 将软件开发过程分成两个主要阶段：模型级和代码级。模型主要关注系统的设计正确 性，包含模型阶段设计、验证系统设计和功能模块设计，从而达到以较小代价修改软 件错误的目的。基于不同编程代码可由模型自动生成，将程序员从繁杂的代码编程过 程解脱出来，也避免了功能模块由于编程语言的更迭而重复开发。m d a 方法将代码的 开发提升到了模型层次，因此传统的工具集不能满足m d a 方法的需求，需要把模型 工具、原有的传统开发工具以及与应用领域相关的工具有机的结合起来，形成一个基 于模型的面向领域的嵌入式生产线开发环境。所谓嵌入式模型开发环境1 3 】，就是把传统 的开发工具和具体应用领域的工具集成起来的，包含建模、仿真、验证、代码生成、 测试等嵌入式软件开发全过程的开发平台，这个流程就是了基于模型的嵌入式软件生 产线。 在这条软件生产线的生产过程中，模型驱动验证是个重要的环节( 这里主要是 对系统的非功能属性进行验证) ，通过验证提前发现存在问题，可以大大地减少后期的 工作量。而对于嵌入式非功能属性的验证中，实时性验证是必须的，高级的嵌入式系 统对时间有着很高的要求，这类系统也常常称为嵌入式实时系统。实时系统的最大特 点是在特定的时间约束内完成特定的行为动作，该特定的时间约束包括响应时间、执 行时间、截止时间、任务周期等等。要确保这类系统的安全性和正确性是非常有必要 的，任何一个错误都会带来重大的经济损失、环境的破坏、甚至生命安全。对于这类 系统就是要求在它们合法是时间内完成相应的行为，不会发生超时现象，确保系统的 可调度性。目前，嵌入式实时系统在对正确性和安全性有严格要的领域中得到广泛的 西南交通大学硕士研究生学位论文第2 页 应用，这些系统的开发成本也相对比较高，因此要是在系统开发过程中能够尽早的检 验出问题，就可以节省大量的人力物力。 对于系统非功能的验证，如果没有计算机辅佐软件的帮助，对系统的分析和验证 会变得很复杂。而实时系统的最大的一个特点是必须在严格的时间约束下作出相应的 响应，这就是说系统的正确性不但依赖于系统中各个部分状态相互作用，而且还依赖 这些状态发生的时间。换句话说，对于实时系统的验证结果不仅要求满足逻辑上是正 确的，还要求满足在时间上也是正确的。 因此本文在基于模型的嵌入式生产线的研究中，把重点放在研究和解决模型驱动 方面的形式化验证问题，对嵌入式实时性系统中的任务的调度问题进行研究。对于这 种模型验证的方法最早是由c l a r k 和e m e r s o n 提出，其基本原理是为要检测的系统建立 形式化模型，阐明所要验证的性质，然后使用算法去检查该模型是否满足所述性质。 模型验证的基本思想是状态空间的穷尽搜索，搜索的可穷尽性依赖于模型状态的有穷 性【4 】。在实际工作中，如：在一个轨道上，两列火车不能同时通过；在航空中，规定某 航班的飞机在某个时间内必须到达某的地方等等。这些性质的验证，往往是转换为状 态可达性的判断问题限6 1 。现在有多种可达性分析方法，本文使用时钟约束的可达性分 析方法c 一，主要通过建立任务的时间自动机的形式化模型，判断时间自动机是否会进 入错误状态，从而分析系统的可调度性。 1 2 国内外情况 当今的嵌入式开发过程强调两方面的因素：复用性( 提高生产效率) 和高可信度 ( 提高软件的安全性) ，这两方面的因素是软件生产工业发展的趋势，国内外大行嵌入 式软件开发商都往这方面研究，力求把自己的产品做到最好。而模型驱动概念的出现， 恰好地跟这两方面的问题不谋而合，给这两方面的问题提出切实可行的解决方法。模 型驱动重点放在模型的建立和模型的验证上。只要所建立模型是正确的，以后平台或 编译语言的变更，都可以根据不同的转换规则由模型自动生成基于新平台上或新的编 译语言的代码程序，避免由于平台和编程语言的更迭而重复开发，同样的转换规则可 以被应用到不同的系统开发工作中，这样就很大程度上延长了系统的生命周期【1 0 】，实 现开发的复用性。前面强调所建立的模型的正确性，这就需要对模型进行验证，检测 模型的可信度，通过模型所建立的系统，需要考虑它的非功能属性，其中实时性是嵌 入式实时系统的硬性要求，通过检查系统中任务元素的调度问题来反应系统的实时性。 因此本文强调的模型驱动验证是对系统模型中的可调度问题的研究。 1 2 1 模型驱动 为了解决软件开发中出现的种种问题，全球最大的软件工业标准化组织在2 0 0 1 年 西南交通大学硕士研究生学位论文第3 页 7 月提出了模型驱动框架m d a 开发方法1 2 l l 】。m d a 是一种基于诸如统一建模语言( u m l ) 【：】、可扩展标记语言( ) ( m l ) 【1 4 】和公共对象请求代理体系结构( c o r b a ) b 5 i 等一系列业 界开放标准的框架，因此她具备软件设计和模型的可视化、存储和交换的功能。和u i v l l 相比，m d a 能够创建出机器可读和高度抽象的模型，这些模型独立于实现技术，以标 准化的方式储存1 1 1 1 6 1 。如a 把建模语言用作一种编程语言而不仅仅是设计语言。m d a 的关键之处是模型在软件开发中扮演了非常重要的角色。这些模型被划分为两个较大 的抽象层次：平台无关模型( p l a t f o r mi n d e p e n d e n tm o d e l ，p i m ) 和平台相关模型( p l a t f o r m s p e c i f i cm o d e l 。p s m ) 。p i m 描述了待开发系统的行为需求，但是不涉及如何在具体的平 台上实现这个系统；p s m 包含了所有在p i m 中表示的功能，并添加了针对实现平台的设 计因素。在m d a 开发方法中，开发人员的主要工作是全面精确地描述系统的p i m ，并根 据特定的模型转换规则集合由p i m 自动转换得到p s m t l 6 1 。 m d a 是一种系统开发方法，提供一种利用模型去指导分析、设计、构建、部署、 操作、维护和更新的手段，m d a 的三个主要目标是：通过架构性的分离来实现轻便性、 互操作性和可重用性。m d a 理论还处在一个探索期，很多理论和方法并不成熟，当然 无从谈起有成熟的工具，从目前的趋势而言，从理论到实际的工具都离o m g 组织所 提出的预想有较大距离。目前，无论是在国外还是国内，对m d a 都只是处在一个起 步阶段【堋。 m d a 的出现，为提高软件开发效率，增强软件的可移植性、协同工作能力和可维 护性，以及文档编制的便利性指明了解决之道。m d a 被面向对象技术界预言为未来两 年里最重要的方法学。当今建模的主要问题在于，对于很多企业来说它只是纸面上的 练习。这就造成了模型和代码不同步的问题，代码会被不断修改，而模型不会被更新， 这样模型就失去了意义。弥补建模和开发之间的鸿沟的关键就在于将建模变为开发的 一个必不可少的部分。m d a 是模型驱动开发的框架，m d a 的远景是定义一种描述和 创建系统的新的途径。m d a 使得u m l 的用途走得更远，而不仅仅是美丽的图画。很 多专家预言m d a 有可能会带领我们进入软件开发的另一个黄金时代。 1 2 2 模型驱动验证 在模型开发过程中强调模型的可行度问题，确保所开发的系统的正确性和可靠性， 使用形式化验证方法是十分必要的。而在1 1 节中提到，对系统的可调度性分析是十分 必要的。 时间自动机的性质已经得到比较充分的研究【1 8 2 0 。时间自动机模型也被进一步的扩 展，提出了概率时间自动机1 2 1 ，时间i 0 自动机 z 2 l ，线性时间自动机，时间树自动机1 等新的模型。不过主要的研究方向还是基于时间自动机的模型验证。基于时间自动机 已经开发出了多种自动验证工具，如u p p a a l ，k r o n o s ，c o s p a n 等。 西南交通大学硕士研究生学位论文第4 页 近年来，利用时间自动机对实时系统进行形式化验证技术有了一定的发展。其中 以时间自动机作为行为模型的形式化验证工具u p p a a l 可以有效地对实时系统进行验 证和模拟，从而确保了实时系统在实际运行中的高度正确性。 1 3 课题来源 本课题是国家8 6 3 重点项目( 2 0 0 7 a a 0 1 0 3 0 4 ) 面向嵌入软件的生产线专题的 高可信度生产工具及集成环境，而当中的模型驱动验证也是国家自然基金项目 ( 9 0 7 1 8 0 1 9 ) 嵌入式软件可信属性分析和验证。 1 4 本文研究内容及论文结构 1 4 1 本文研究内容 本文研究的是基于模型驱动验证及开发的嵌入式软件生产线开发环境，在现有的 嵌入式集成开发环境l a m b d a p r o 的基于上集成模型验证工具、模型开发工具和其他的 第三方工具。要实现一个包含建模、仿真、验证、代码生成、测试等嵌入式软件开发 全过程的开发平台。 对于基于模型的嵌入式软件生产线中，模型验证是一个重点，关系着生产线的往 下开发进度和影响着系统的质量。而本文所提到的模型验证主要是对系统的可调度问 题进行分析，也就是任务的状态迁移问题的分析，任务会不会在某个时刻迁移到错误 状态( 发生超时现象) 。这种从某个时刻到另外一个时刻状态的活动情况的研究，就是 时间自动机位置迁移的研究。而时间自动机理论就是一种提供了一个形式化的方法去 建模和分析实时系统的行为，系统的正确性必须遵守和保证多方面的时间约束，比如： 执行时间，响应时间，任务频率，通信延时等等。对于在时间自动机上是否能从某个 状态上迁移到另外某个状态上，这就是时间自动机可达性研究的问题。而目前在设计 阶段的形式化调度分析仍是一个新的研究领域，因此本文需要开发一个使用形式化分 析方法的调度检测工具。对调度检测工具所分析系统模型进行研究，设计一个具有普 遍性的系统模型，具备分析大部分的嵌入式系统。研究自动机理论，对所分析的系统 任务进行形式化模型设计。并研究标准的可达性算法，对调度算法和仿真算法的研究 设计，实现调度检测工具。 在这条嵌入式软件生产线上，除了模型验证外，还需要包含建模、代码生成、测 试等其他的开发过程。因此需要研究工具间的无缝集成技术，使得所有功能都在一个 开发环境下完成。由于集成开发环境l a m b d a p r o 是基于e c l i p s e 框架，因此需要研究 e c l i p s e 框架结构，和插件开发技术，和第三方工具。 西南交通大学硕士研究生学位论文第5 页 1 4 2 论文结构 第一章绪论。介绍本课题的背景及意义，介绍国内外的研究概况，并介绍课题的 来源，最后介绍了本文研究内容。 第二章基于模型的嵌入式软件生产线的需求的设计。分析了整个生产线生产过程 中所需要完成的工作，以及需要集成的工具，为设计与实现提供依据。 第三章调度分析系统模型的设计。对调度检测工具s c t 所分析的系统进行设计， 其中主要对任务的行为自动机进行设计。为调度检测工具的调度仿真过程算法提供准 备。 第四章调度检测工具s c t 的设计与实现。对s c t 工具的各个部分进行设计，重点 实现系统调度仿真算法分析部分。 第五章基于模型的嵌入式软件生产线的设计与实现。根据需求，设计与实现生产 线的各个环节。 第六章软件生产线开发环境的验证。通过一个例子在基于模型的嵌入式生产线上 的应用，来说明和验证这个开发过程。 西南交通大学硕士研究生学位论文第6 页 第2 章基于模型的嵌入式软件生产线需求分析 目前国外已经有一些基于模型的嵌入式软件生产线开发环境，如m a t h w o r k s 公司 的s i m u l i n k 环境【2 町，i - l o g i x 公司的r h a p s o d y t 5 】，法国爱斯特尔技术公司的s c a d e t 2 6 ： s i m u l i n k 提供一个动态系统建模、仿真、综合分析和特定环境的代码生成的集成环境。 它具有适应面广、结构和流程清晰及仿真精细、贴近实际、效率高、灵活等优点。但 不能直接对系统级别的非功能属性进行验证；r h a p s o d y 也包含嵌入式软件开发的全过 程，完全遵循u m l 标准、独特的模型代码相关性技术以及图形化的、设计级的调试 和验证技术。它提供了可视化的开发环境，贯穿了工程化的设计思想，使用了自动化 的开发模式，并支持团队化的协作开发。但不具备模型驱动形式化验证功能，而且模 型类型繁多，最后转换成嵌入式代码需要做复杂的处理；s c a d e 运用了c o r r e c tb y c o n s t r u c t i o n 的概念，覆盖了嵌入式软件开发中从需求到嵌入式代码的整个流程。为了 弥补自身的不足，s c a d e 引入了桥接技术，可以与其他的工具进行桥接，比如与 s i m u l i n k 的桥接，可以把s i m u l i n k 的模型转换成自己的模型，丰富了s c a d e 的建模 内容。同样s c a d e 也有对r h a p s o d y 的桥接。s c a d e 功能强大，在很多的大型项目上 得到成功的应用。但是s c a d e 的使用相当复杂，而且跟s i m u l i n k 一样不能对系统级 别的非功能属性进行验证；此外o c a r i n a 是基于a a d l 语言的开源工具，该工具主要 用来对a a d l 模型的处理，包括模型的构建，模型的调度分析，代码生成。但o c a r i n a 没有可视化的界面，使用不方便，o c a r i n a 可以从体系结构上建模系统的非功能要求， 不能对系统的具体功能行为进行建模，需要人工手写功能代码。 国内目前对嵌入式模型开发环境还处于初步应用阶段，不少院校和研究所都在开 展建模方面的研究工作，但尚未形成一个完整的建模、仿真、验证、代码生成、测试 等嵌入式软件开发环境。因此针对上述问题，本课题对基于模型开发并具备对系统模 型非功能属性形式化验证的嵌入式生产线进行研究和实现。 2 1 生产线的生产流程 所谓基于模型的嵌入式软件生产线就是一个集成开发环境，其生产流程就是把一 些模型零件，经过各种方法的加工，最后组合起来成为一个完整的产品。每一种的加 工都是由特定人员和软件完成，可以独立同步进行，这样提高了生产效率。 基于模型的嵌入式软件生产线开发环境，有别于以往的那些基于代码为主线的开 发环境，生产线必须以模型开发为基线，开发过程包含模型建立，模型仿真验证，代 码生成，测试等过程。这也是一个集成环境，需要集成第三方工具来完成这一系列的 开发过程。 如图2 1 是基于模型的嵌入式生产线的生产流程： 西南交通大学硕士研究生学位论文第7 页 图2 1 生产线的生产流程 l a m b d a p r o 集成开发环境是由北京科银京成技术有限公司开发的一个面向智能 电子设备的专业嵌入式软件开发平台，因此基于该平台集成了自主研发的工具( 如 u c a g t ：，】代码转换器、s c t ( s c h e d u l i n gc h e c kt 0 0 1 ) 调度检测工具) 和第三方的开发工 具。l a m b d a p r o 平台是基于e c l i p s e 架构进行设计，主要由两部分组成：d e l t a o s 和 l a m b d a t o o l 。 l a m b d a t o o l 是嵌入式软件平台l a m b d a p r o 的开发环境，为嵌入式软件开发者 提供编辑环境、系统配置、编译环境、目标机管理、调式环境和团队开发等相关工具。 d e l t a o s 是一个高可靠嵌入式实时操作系统，是智能电子设备软件的核心，已经在 国防和民用的电子设备中得到广泛的应用，特别是d e l t a o s 已经被成功应用于航空航 天的高可靠性设备。它的组件包括：实时操作系统内核、文件系统、网络协议栈、图 形用户接口。d e l t a o s 系统支持多种嵌入式微处理器，如：a r m 7 、s t r o n g a r m 、p p c 8 x x 、 p p c 4 x x 、x 8 6 、m i p s 等。 由于基于模型的嵌入式软件生产线是在l a m b d a p r o 的基础上集成了本课题前期自 主开发的软件和第三方开发软件，因此基于模型的生产线开发环境叫做l a m b d a m d e ( m o d e ld e v e l o p m e n te n v i r o n m e n t ) 。如图2 1 是开发人员使用l a m b d a m d e 环境开发 嵌入式系统的开发过程，及这个过程中产生的相关文件。每个阶段过程都会产生相关 的文件，并对这些文件进行验证测试，才能进行下一步的开发，而系统模型和功能模 型的开发可以并行进行。这种开发方法能够提高系统的可靠性，减少错误。一开始通 过o s a t e 构建系统框架模型a a d l ，通过s c t 分析系统框架模型的调度性，实时性 符合要求后使用u c a g 工具把a a d l 转换成c 代码；通过s i m u l i n k 建立功能模型， 对功能模型进行静态测试和覆盖测试，符合测试要求后，把功能模型转换成c 代码。 通过代码合成器把框架代码和功能代码合成起来形成一个完整的系统程序，最后通过 编译下载到目标机中。 西南交通大学硕士研究生学位论文第8 页 2 2 开发过程需求 2 2 1 向导需求 每个开发工具的项目工程都有自己所属的向导来指引用户创建他们所需的项目， m d e 项目也不例外，需要在l a m b d a m d e 开发工具中带有该项目所属的向导，通过向 导生成该项目特有的目录结构。 2 2 2 集成模型开发工具的需求 当今嵌入式系统发展迅速，系统的复杂度越来越大，系统除了功能越来越复杂， 系统的非功能属性也日益受到重视，而且被开发人员放到第一位考虑。其中嵌入式系 统的非功能属性包含：可用性、实时性、响应性、吞吐量、防危性和可靠性。那么模 型就要求能够体现出这些非功能需求，并且能够具有功能模型的设计。当具备上面两 种条件的模型才是一个完整的模型，才符合本文嵌入式生产线的需求。 目前还没有任何一种的模型同时满足非功能属性和功能属性的两个要求。比如我 们使用比较频繁的u m l 模型，从它诞生到今天，经过人们不断的发展和改进，已经具 备很强的能力，但它不适用于嵌入式模型开发，它也不具备描述系统非功能属性的能 力。在这样的情况下，我们需要选择一个具备描述嵌入式系统非功能属性的模型和一 个具备描述系统具体功能属性的模型相结合，来构造一个完整的嵌入式系统模型。 在这样的前提下，本课题的嵌入式软件生产线选择了两种模型相结合：一种是 a a d l 模型，一种是s i m u l i n k 模型。a a d l 模型是一种对系统体系结构建模的模型， 但是该模型不能描述系统的任何功能行为。而s i m u l i n k 模型是一种建模系统具体功能 行为的模型，两者的结合能够完整描述一个系统，因此根据a a d l 模型和s i m u l i n k 模 型各自的优点与缺点，把两种模型结合起来，形成一套完善的模型开发方法。 a a d l t 丝- 3 0 l ( a r c h i t e c t u r ea n a l y s i s & d e s i g nl a n g u a g e ) 是一种字符化和图形化的语 言，由s a e ( s o c i e t yf o ra u t o m o t i v ee n g i n e e r s ) 体系结构描述语言附属委员会等组织提 出，用于建模性能关键的实时系统的软硬件体系结构。使用a a d l 的目的在于提供一 个标准的和足够精确的建模方法，能够有效地描述系统的非功能属性。允许系统设计 者对组成系统的组件以及系统的可调度性、吞吐量、防危性等进行分析。从这些分析 中，设计者能够评估体系架构的合理性及变化。a a d l 的主要组件 2 9 , 3 0 分为软件组件和 执行平台组件两大类。其中软件组件主要包括数据、线程、进程、子程序等组件；执 行平台组件主要包括处理器、存储器、总线、外设等组件。软件组件和执行平台组件 组合在起可以构成系统模型。对于每种组件，都有组件类型声明和组件实现声明。 s i m u l i n k l 2 l 是m a t h w o r k s 公司提供一个动态系统建模、仿真、综合分析和特定环境 的代码生成的集成环境。s i m u l i n k 据有适应面广、结构和流程清晰及仿真精细、贴近 西南交通大学硕士研究生学位论文第9 页 实际、效率高、灵活等优点，并基于以上优点s i m u l i n k 已被广泛应用于控制理论和数 字信号处理的复杂仿真和设计。s i m u l i n k 是m a t l a b 最重要的组件之一，因此s i m u l i n k 完全支持m a t l a b 中引以为傲的数学模型。它具有一个强大的模型库，能够对很多领域 进行功能建模仿真，不过s i m u l i n k 对嵌入式实时系统中最重要的非功能属性( 调度性、 可靠性、安全性等等) 就无能无力了，因此要引入a a d l 模型进行互补。 因此本生产线需要集成o s a t e ( a a d l 模型开发工具) 和s i m u l i n k 工具，使这两 种工具成为l a