基于SysML活动图的嵌入式实时系统安全性验证方法研究

发布时间：2017-08-07 21:16

  本文关键词：基于SysML活动图的嵌入式实时系统安全性验证方法研究

  更多相关文章： 嵌入式实时系统 安全性 SysML活动图 MARTE时钟 时间自动机 模型检测

【摘要】：嵌入式实时系统在航空航天、核电及交通等安全关键领域中广泛使用,规模变得愈发庞大,体系结构变得更复杂,其故障引起的安全事故有着显著的社会影响,甚至造成灾难性的后果。因此,对嵌入式实时系统设计进行安全性分析与验证成为学术界和工业界亟需攻克的难点。UML(United Modeling Language)常被用来软件设计建模,但在建模能力上不能满足嵌入式实时系统建模需求且缺乏非功能属性建模元素;半形式化的模型在安全性验证上难以被直接使用。针对以上问题,本文提出一种扩展MARTE(Modeling and Analysis of Real-time and Embedded Systems)时钟语义信息到Sys ML(System Modeling Language)活动图(Sys ML/MARTE活动图)的嵌入式实时系统安全性验证方法,弥补了UML在针对嵌入式实时系统建模及验证上的不足。主要内容如下:首先,针对嵌入式实时系统,提出使用Sys ML/MARTE活动图对嵌入式实时系统进行建模,包括采用适合系统建模的Sys ML活动图构建功能流模型及扩展MARTE时钟语义来构建时间非功能属性。然后,通过基于元模型的模型转换方法将Sys ML/MARTE活动图转换到时间自动机,包括:(1)针对Sys ML活动图以及MARTE时钟等建模元素,分别构建其同构的元模型,并在元模型体系中将MARTE语义信息添加到Sys ML活动图,构建时间自动机的元模型;(2)给出Sys ML/MARTE活动图和时间自动机的元模型在类型、行为以及时间等元素上的语义映射规则,给出Sys ML/MARTE活动图嵌套、分支和并发结构到时间自动机的转换规则,将Sys ML/MARTE活动图模型转换为时间自动机模型;(3)通过语法转换,将时间自动机模型转换为模型检测工具UPPAAL可以直接使用的时间自动机文本。最后,根据嵌入式实时系统设计安全需求,提取CTL(computation temporal logic)规约,在UPPAAL下对转换得到的时间自动机进行安全性分析与验证。
【关键词】：嵌入式实时系统 安全性 SysML活动图 MARTE时钟 时间自动机 模型检测
【学位授予单位】：南京航空航天大学
【学位级别】：硕士
【学位授予年份】：2015
【分类号】：TP368.1;TP309
【目录】：

• 摘要4-5
• ABSTRACT5-10
• 缩略词10-11
• 第一章 绪论11-16
• 1.1 课题研究背景及意义11-12
• 1.2 研究现状及选题依据12-14
• 1.2.1 研究现状12-13
• 1.2.2 选题依据13-14
• 1.3 论文组织结构14-16
• 第二章 面向嵌入式实时系统安全性验证的SYSML活动图转换方法16-28
• 2.1 嵌入式实时系统安全性问题分析16-17
• 2.1.1 嵌入式实时系统特点16-17
• 2.1.2 安全性验证的必要性17
• 2.2 基于MDA的模型转换方法17-20
• 2.2.1 纵向模型转换18-19
• 2.2.2 横向模型转换19-20
• 2.3 面向嵌入式实时系统安全性验证的SYSML活动图转换20-27
• 2.3.1 Sys ML活动图特点20-22
• 2.3.2 MARTE时钟结构22-25
• 2.3.3 面向嵌入式实时系统安全性验证的扩展Sys ML活动图转换框架25-27
• 2.4 本章小结27-28
• 第三章 SYSML/MARTE活动图元建模与时间自动机元建模28-43
• 3.1 异构元模型的同构化28-31
• 3.1.1 异构元模型的根-元元模型28-30
• 3.1.2 异构元模型的同构化方法30-31
• 3.2 SYSML/MARTE活动图元建模31-36
• 3.2.1 Sys ML活动图的语法结构31-32
• 3.2.2 Sys ML活动图元建模32-34
• 3.2.3 MARTE时钟元建模34-36
• 3.3 UPPAAL时间自动机元建模36-42
• 3.3.1 UPPAAL时间自动机语法及语义36-38
• 3.3.2 数据类型元建模38-39
• 3.3.3 表达式元建模39-40
• 3.3.4 组成结构元建模40-42
• 3.4 本章小结42-43
• 第四章 SYSML/MARTE活动图到时间自动机的转换43-57
• 4.1 基于AMMA的活动图到时间自动机的元模型转换框架43-46
• 4.1.1 AMMA平台异构模型转换方法43-44
• 4.1.2 AMMA平台异构模型转换实施过程44-46
• 4.2 SYSML/MARTE活动图与时间自动机元模型间语义映射46-49
• 4.2.1 类型结构元素的语义映射46-47
• 4.2.2 活动行为元素的语义映射47-48
• 4.2.3 时间元素的语义映射48-49
• 4.3 SYSML/MARTE活动图与时间自动机的结构转换49-54
• 4.3.1 嵌套结构的转换49-51
• 4.3.2 并发结构的转换51-53
• 4.3.3 分支结构的转换53-54
• 4.4 时间自动机模型到时间自动机文本的语法转换54-56
• 4.5 本章小结56-57
• 第五章 紧急呼叫系统设计安全性验证57-67
• 5.1 紧急呼叫系统需求描述57
• 5.2 紧急呼叫系统SYSML/MARTE活动图建模57-61
• 5.3 紧急呼叫系统SYSML/MARTE活动图到时间自动机转换61-64
• 5.4 紧急呼叫系统设计的安全性验证与分析64-66
• 5.5 本章小结66-67
• 第六章 总结与展望67-69
• 6.1 论文工作总结67
• 6.2 进一步工作67-69
• 参考文献69-75
• 致谢75-76
• 在学期间的研究成果及发表的学术论文76

【相似文献】

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

1 齐建业;李强;余祥;;基于形式活动图的协议一致性测试用例生成方法研究[J];安徽大学学报(自然科学版);2013年03期

2 管昌生，夏红霞，刘定飞，，钟珞;一种结构程序设计与分析的工具[J];微电子学与计算机;1994年05期

3 王智群;;一种Concur任务树转化为UML2.0的方法[J];计算机工程;2009年11期

4 张正,刘建华,吴洁明,袁山龙;利用UML活动图进行业务分析[J];北方工业大学学报;2003年03期

5 周新宽;陈平;李青山;;一种UML活动图的逆向恢复方法[J];计算机工程与应用;2006年17期

6 孙自安,周伯生;UML活动图的评价和扩展[J];计算机工程与应用;2001年12期

7 杜薇,刘伟;UML的活动图及其在电子政务项目中的应用[J];计算机工程;2003年05期

8 崔萌 ,李宣东 ,郑国梁;UML实时活动图的形式化分析[J];计算机学报;2004年03期

9 朱雪阳,唐稚松;UML活动图的时序逻辑语义[J];计算机研究与发展;2005年09期

10 许永峰;陈平;;基于UML活动图的进程关系模型恢复方法[J];电子科技;2006年05期

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

1 唐剑文;;基于UML嵌套活动图的回归测试用例选择[A];全国第21届计算机技术与应用学术会议（CACIS·2010）暨全国第2届安全关键技术与应用学术会议论文集[C];2010年

2 韦银星;张申生;曹健;;基于UML活动图的软件过程模型研究[A];第六届全国计算机应用联合学术会议论文集[C];2002年

3 陈章耀;李晓峰;;基于UML活动图的电信业务过程建模方法[A];2008'中国信息技术与应用学术论坛论文集（一）[C];2008年

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

1 记者 朱周良;美再谋划时代突破：斥巨资绘人脑活动图[N];上海证券报;2013年

2 本报记者 沈湫莎;绘制人脑活动图，10年太短[N];文汇报;2013年

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

1 朱羿全;安全关键嵌入式系统的SysML活动图概率验证方法研究[D];南京航空航天大学;2015年

2 常旭岭;基于Petri网的“系统的系统”的建模与仿真的研究[D];上海交通大学;2015年

3 惠文涛;基于概率模型检测的SysML活动图验证方法研究[D];解放军信息工程大学;2015年

4 俞磊;基于UML活动图的仿真与测试方法研究[D];南京大学;2014年

5 李庆;基于UML活动图的测试用例生成方法的研究[D];江苏科技大学;2016年

6 黄传林;基于SysML活动图的嵌入式实时系统安全性验证方法研究[D];南京航空航天大学;2015年

7 胡良文;基于SPIN的UML模型一致性验证的研究及应用[D];南京航空航天大学;2015年

8 曹伟芳;基于SysML活动图的测试序列生成方法研究[D];南昌航空大学;2016年

9 王志超;面向活动图的代码自动生成技术研究[D];哈尔滨工业大学;2010年

10 丁娜;带OCL约束的活动图多态测试方法的研究[D];重庆大学;2012年

本文编号：636747