基于AADL的综合航电系统资源配置安全性分析与验证

发布时间：2017-09-15 16:18

  本文关键词：基于AADL的综合航电系统资源配置安全性分析与验证

  更多相关文章： 综合航空电子系统 基于模型驱动 ARINC653标准 AADL模型 可靠性分析 可调度性分析

【摘要】：资源配置是综合航空电子系统(IMA)设计的重要环节,而配置信息是航空电子系统中的重要内容,它存储了系统软硬件的参数信息,若配置信息发生错误则会导致系统无法正常运行,甚者会引发大型事故,所以配置信息的安全性分析显得尤为重要,尤其是对其进行可靠性和可调度性验证。随着嵌入式系统的规模越来越复杂以及安全需求的不断提升,基于模型驱动的开发方法成为主流,而AADL也是现如今嵌入式实时系统领域模型驱动的新标准,能更好地支持嵌入式系统软硬件相结合的模型的建立,还能够对系统的可靠性、实时性等非功能属性进行很好的描述,因而在航空电子系统领域得到了广泛的应用。针对IMA系统配置信息的安全性验证以及该配置信息对应的IMA系统安全性分析的问题,本文基于AADL语言,在模型驱动开发方法下完成的主要工作如下:(1)分析了AADL模型元素和ARINC653配置信息的语义相似性,给出配置信息主要的核心概念与AADL模型元素的转换规则,基于这些转换规则将配置信息转换成AADL模型,并使用REAL设计了相应的可靠性验证定理。(2)分析了转换后的AADL模型,采用时间自动机形式化模型检验方法,设计了线程模板和调度器模板,根据转换法则将AADL调度模型转换到时间自动机模型,依据配置信息中系统可调度性验证需求,在工具UPPAAL中对转换得到的时间自动机进行模拟和验证,等价地验证原模型的可调度性。(3)利用Eclipse插件开发技术,设计了配置信息转换与验证插件并将其集成到了AADL建模与分析工具OSATE中,该插件具备如下功能:输入配置信息文件,转换成AADL模型后,结合REAL定理和Ocarina工具验证配置信息的可靠性;通过文件解析,转换生成时间自动机模型文件和性质验证查询文件,自动调用UPPAAL工具验证模型的可调度性。并给出了具体实例验证了工具的正确性。(4)在资源配置AADL模型的基础上,利用工具OSATE对该资源配置所支持的应用操作层和功能层进行建模和分析,同时使用AltaRica语言建立失效模型,结合工具SimFia自动生成故障树。
【关键词】：综合航空电子系统 基于模型驱动 ARINC653标准 AADL模型 可靠性分析 可调度性分析
【学位授予单位】：南京航空航天大学
【学位级别】：硕士
【学位授予年份】：2016
【分类号】：V243;TP309
【目录】：

• 摘要4-6
• ABSTRACT6-14
• 第一章 绪论14-18
• 1.1 研究的背景与意义14-15
• 1.2 国内外研究现状及存在的问题15-17
• 1.3 主要研究内容与论文结构17-18
• 第二章 相关基础知识18-34
• 2.1 综合模块化航电系统体系结构概述18-19
• 2.2 ARINC653软件体系结构19-20
• 2.3 AADL20-27
• 2.3.1 组件（Component）21
• 2.3.2 组件类型（Component Type）21-22
• 2.3.3 组件实现（Component Implementation）22-23
• 2.3.4 组件交互（Components Interactions）23-25
• 2.3.5 模式（Modes）25
• 2.3.6 流（Flows）25-26
• 2.3.7 属性（Properties）26
• 2.3.8 AADL模型工具26-27
• 2.4 时间自动机27-29
• 2.4.1 时间自动机理论27-28
• 2.4.2 基于时间自动机的验证28-29
• 2.5 UPPAAL29-31
• 2.6 Alta Rica31-32
• 2.7 基于模型驱动的安全性分析过程32-33
• 2.8 本章小结33-34
• 第三章 IMA系统配置信息的转换与验证34-48
• 3.1 IMA系统配置信息转换为AADL模型34-43
• 3.1.1 转换规则35-41
• 3.1.2 模型转换实例41-43
• 3.2 配置信息可靠性验证43-47
• 3.2.1 REAL语言43-45
• 3.2.2 时间约束45
• 3.2.3 空间约束45-46
• 3.2.4 健康监控约束46-47
• 3.3 本章小结47-48
• 第四章 AADL调度模型的转换与验证48-59
• 4.1 引言48-49
• 4.2 AADL调度模型与时间自动机模型的映射关系49-52
• 4.2.1 调度模型的形式化语义49-50
• 4.2.2 线程状态转换机制50-51
• 4.2.3 调度模型到时间自动机的语义映射51-52
• 4.3 调度模型时间自动机设计52-56
• 4.3.1 线程模板52-53
• 4.3.2 调度器模板53-56
• 4.4 可调度性验证语句56-57
• 4.5 调度模型到时间自动机模型的转换实例57-58
• 4.6 本章小结58-59
• 第五章 IMA系统配置信息转换与验证工具的实现59-72
• 5.1 引言59
• 5.2 配置信息文件解析59-61
• 5.3 AADL模型生成及验证61-63
• 5.4 UPPAAL模型文件生成63-64
• 5.5 插件开发技术64-67
• 5.6 实例分析67-71
• 5.6.1 配置信息可靠性验证67-69
• 5.6.2 配置信息可调度性验证69-71
• 5.7 本章小结71-72
• 第六章 IMA资源配置安全性分析与验证72-77
• 6.1 应用操作层模式枚举72-74
• 6.2 功能层建模74-76
• 6.3 本章小结76-77
• 第七章 总结及未来展望77-78
• 7.1 工作总结77
• 7.2 未来展望77-78
• 参考文献78-82
• 致谢82-83
• 在学期间的研究成果及发表的学术论文83

【相似文献】

中国期刊全文数据库 前10条

1 刘柏;唐龙利;;舰船安全性分析技术研究[J];电子产品可靠性与环境试验;2006年05期

2 王喜奎;刘春雷;;可靠性工程师资格考试辅导教材之六——安全性[J];质量与可靠性;2008年04期

3 赵子建;任璐璐;;关于飞机区域安全性分析评价模型的构建[J];科协论坛(下半月);2012年04期

4 冯福来;飞机区域安全性分析[J];航空标准化与质量;1994年03期

5 单晨;孙景峰;;一卡通主要卡片的安全性分析[J];智能建筑;2009年10期

6 刘晓;蒋睿;;移动云计算中弹性存储外包方案的安全性分析和改进(英文)[J];Journal of Southeast University(English Edition);2012年04期

7 李晓磊;田瑾;赵廷弟;;改进的区域安全性分析方法[J];航空学报;2008年03期

8 杨建蓉,孟立,王跃鸿;地区电网调度自动化系统安全性初探[J];山西电力;2005年03期

9 云平;姜红旗;梁海燕;;大坡度滑索安全性分析[J];起重运输机械;2011年08期

10 熊峻江,刘宝成,高宏;系统安全性分析与设计方法研究[J];北京航空航天大学学报;2002年02期

中国重要会议论文全文数据库 前10条

1 文晓阳;高能;荆继武;;论坛验证码技术的安全性分析[A];全国计算机安全学术交流会论文集（第二十二卷）[C];2007年

2 王丹琛;何大可;;密写系统的安全性研究[A];2006中国西部青年通信学术会议论文集[C];2006年

3 范涛;鲍先巡;吴传华;常劲松;彭代银;;桑资源饮品的研究——灵芝桑茶的理化品质与安全性分析[A];中国蚕学会第七次全国代表大会论文集[C];2003年

4 张兆心;方滨兴;胡铭曾;张宏莉;;基于SIP网络的安全性研究[A];全国网络与信息安全技术研讨会'2005论文集（上册）[C];2005年

5 查月;高磊;;TCP/IP协议的安全性分析与防御[A];2008-2009年船舶通信导航论文集[C];2009年

6 林曦;高文建;何朝阳;薛峰;许剑冰;徐泰山;薛禹胜;汪磊;;广西电网在线动态安全性分析系统[A];第三届广西青年学术年会论文集（自然科学篇）[C];2004年

7 林曦;高文建;何朝阳;薛峰;许剑冰;徐泰山;薛禹胜;汪磊;;广西电网在线动态安全性分析系统[A];广西电机工程学会第八届青年学术年会论文集[C];2004年

8 海培华;;浅谈GSM手机的安全性[A];中国通信学会第五届学术年会论文集[C];2008年

9 马瑞萍;;SSL安全性分析研究[A];第十六次全国计算机安全学术交流会论文集[C];2001年

10 陈伟杰;林宏基;;SOAP的安全性分析与整合[A];全国第16届计算机科学与技术应用（CACIS）学术会议论文集[C];2004年

中国重要报纸全文数据库 前3条

1 ;如何提高SQL Server的安全性？[N];网络世界;2008年

2 中国科学院动物研究所研究员 沈孝宙;关于GMO的对话[N];中国国门时报(中国出入境检验疫报);2001年

3 北京 Analysist;ExGB GuestBook安全性分析[N];电脑报;2001年

中国博士学位论文全文数据库 前10条

1 张源;安卓平台安全性增强关键技术的研究[D];复旦大学;2014年

2 周淳;有限长诱骗态量子密钥分配安全性研究[D];解放军信息工程大学;2014年

3 宋辉;隐密安全性机理研究[D];大连理工大学;2011年

4 赵义博;量子密钥分配的安全性研究[D];中国科学技术大学;2009年

5 柴震川;门限密码方案安全性和应用研究[D];上海交通大学;2007年

6 汪朝晖;椭圆曲线密码的安全性研究[D];武汉大学;2004年

7 范伟;移动商务安全性研究[D];北京邮电大学;2010年

8 孙艳宾;公平交换协议的设计与安全性研究[D];北京邮电大学;2011年

9 余斌霄;无线网络的安全性[D];西安电子科技大学;2006年

10 孔鸿滨;语义Web技术的本体安全性研究[D];云南大学;2012年

中国硕士学位论文全文数据库 前10条

1 王晶;SSL/TLS的侧信道攻击[D];山东大学;2015年

2 温轩;实际QKD系统的安全性分析[D];哈尔滨工业大学;2015年

3 牛磊;云存储中数据审计协议的分析与设计[D];电子科技大学;2014年

4 李文宇;城市道路无标记路段穿越安全性研究[D];北京交通大学;2016年

5 邢逆舟;基于模型的综合化航电系统资源配置安全性分析与研究[D];南京航空航天大学;2015年

6 孙健;基于AADL的综合航电系统资源配置安全性分析与验证[D];南京航空航天大学;2016年

7 陈龙;IMA重配置策略和重配置的安全性分析方法研究[D];南京航空航天大学;2016年

8 张贵;面向适航认证的综合化航电系统架构安全性评估方法研究[D];南京航空航天大学;2016年

9 李军;舰船典型系统安全性分析评估方法研究[D];哈尔滨工程大学;2012年

10 张旭光;火箭滑橇设计结构安全性分析[D];南京理工大学;2012年

，

本文编号：857588