浅谈aadl模型可调度性分析工具设计与实现

《浅谈aadl模型可调度性分析工具设计与实现》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、西南交通大学硕士学位论文AADL模型可调度性分析工具设计与实现姓名：刘倩申请学位级别：硕士专业：计算机系统结构指导教师：李允20100401摘要随着计算机应用领域的不断扩张，计算机软件的开发规模逐渐扩大，软件复杂度不断增加，开发周期和开发成本也不断增长。为了解决这些问题，对象管理组织(OMG)提出了模型驱动结构方法(ModelDrivenArchitecture)[51。MDA的核心思想是以模型为中心，将模型和实现分离，使软件开发过程简化为建立业务逻辑模型后由机器自动生成特定计算平台的代码。在MDA中，建模语言不仅仅是设计语言，也是编程语言。针对嵌入式领域中的

2、软件开发复杂度问题，业界提出一种基于MDA方法的体系结构建模语言一体系结构分析设计语言(觚mtec觚AnalysisandDesignLanguage，AADL)11][2][31。AADL是用于设计和分析安全关键的嵌入式实时系统的软件和硬件体系结构的建模语言，围绕AADL的开发平台及模型验证工具的开发逐渐成为热点。MDA的核心是模型，而模型设计是否满足需求则需要其它工具来进行测试验证。本论文基于带时钟约束的混合自动机理论，设计了一种对AADL模型的可调度性进行形式化验证的工具。论文首先介绍了目前关于AADL模型的可调度性验证的研究情况及已开发的工具，并分析了

3、各种工具的缺陷。然后简要介绍了AADL的概念及时间自动机理论。在此基础上，对使用UPPAAL工具对AADL模型进行可调度性验证进行了实践。实践表明UPPAAL工具无法进行可抢占调度策略下的AADL模型的可调度性验证。因此，论文在带时钟约束的混合自动机理论基础上进行了AADL可调度性验证工具UCaS的设计开发。论文按照软件工程方法分模块详细说明UCaS的设计、涉及的技术及关键代码，并对UCaS工具的性能进行了测试。论文最后总结了UCaS工具的优点及局限性，对AADL模型验证工具的后继研究和发展进行了展望。关键词：模型驱动开发；AADL模型；UCaS；时间自动机；

4、带时钟约束的混合自动机；可达性验证：UPPAAI，工具AbstractAsthefieldofapplicationbasedoncomputerextendsincreasingly,thescaleofdevelopingcomputersoRwareandthecomplexityofsoRwareincrease，soitisthesame谢tllthetimeandcostofdeveloping．Aimingatsolvingtheseproblems，ObjectManagementGroup(OMG)proposesModelDrivenArc

5、hitecture(MDA)．ThecoreideaofMDAistoseparatethemodel诚tlltherealization，sothattheprocedureofsoftwaredevelopingCanbesimplifiedintobuildingupbusinesslogicalmodelthencreatingcodeonspecificcomputingplatformautomaticallybymachine．Therefore，themodelinglanguageinMDAisnotonlydesigninglanguage

6、butalsoprogramminglanguage．TheindustryhasputoutamodelinglanguagebasedonMI)Amethodfordevelopingembeddedsystemsoftware⋯ArchitectureAnalysisandDesignLanguage(AADL)，againstthesimilarproblemsfromthesoftwarecomplexity．AADLisamodelinglanguagewhichcanbeusedtodesignandanalyzethesoftwareandha

7、rdwarearchitectureofperformance-criticalreal-timesystems．11ledevelopingplatformandthemodelverificationtoolaroundAADLarebecomingthedevelopinghotpoim．mmostimportantpartinMDAismodel，whichneedsothertoolstotestifthedesigningfitstheoriginaldemand．Thisthesisisbasedonhybridautomaton、Ⅳitllre

8、lativetimeconstrain