基于AUTOSAR存储保护机制的形式化建模与分析

发布时间：2017-10-15 08:30

  本文关键词：基于AUTOSAR存储保护机制的形式化建模与分析

  更多相关文章： 形式化建模 模型检测 汽车电子规范 存储保护机制 通信顺序进程

【摘要】：随着汽车生产规模的不断扩大,基于汽车开放系统架构AUTOSAR (AUTomotive Open System Architecture)标准也越来越普及。人们对于基于AUTOSAR规范的存储保护机制的研究逐步深入,如何才能提高汽车存储保护规范的安全性是当下值得研究的问题。本文使用形式化建模语言CSP对基于AUTOSAR规范的内存保护机制以及操作系统应用的运行机制进行建模。为了验证模型符合AUTOSAR应用运行机制中可信应用和非可信应用调用系统服务的规范、存储保护机制中应用、任务、中断服务子例程访问各个存储模块的规范,使用线性时态逻辑公式(LTL:Linear Temporal Logic)对描述相关性质并进行验证,并使用模型检测工具AT(Process Analysis Toolkit)证明模型满足无死锁性、安全性、活性等性质。运用形式化方法对AUTOSAR存储保护机制建模可以确保系统安全性,从逻辑上讨论AUTOSAR存储保护机制的正确性对汽车电子操作系统的安全性提供了可靠支持。
【关键词】：形式化建模 模型检测 汽车电子规范 存储保护机制 通信顺序进程
【学位授予单位】：华东师范大学
【学位级别】：硕士
【学位授予年份】：2016
【分类号】：U463.6
【目录】：

• 摘要6-7
• Abstract7-13
• 第1章 绪论13-17
• 1.1 研究的背景13-14
• 1.2 形式化方法14-15
• 1.3 本文的研究内容和研究意义15
• 1.3.1 研究内容15
• 1.3.2 研究意义15
• 1.4 本文的主要贡献15-16
• 1.5 本文的组织结构16-17
• 第2章 相关研究现状及预备知识17-21
• 2.1 国内外相关研究现状17-18
• 2.2 预备知识18-20
• 2.2.1 通信顺序进程18-19
• 2.2.2 线性时态逻辑19
• 2.2.3 PAT工具19-20
• 2.3 本章小结20-21
• 第3章 总体架构和总体建模21-25
• 3.1 研究框架21-23
• 3.1.1 存储保护机制22
• 3.1.2 应用及其状态转换过程22-23
• 3.2 总体建模23-24
• 3.3 本章小结24-25
• 第4章 基于AUTOSAR存储模块的建模与分析25-43
• 4.1 AUTOSAR OS存储保护机制25-28
• 4.2 AUTOSAR OS存储形式化建模28-41
• 4.2.1 存储保护架构28-30
• 4.2.2 存储模块建模30-31
• 4.2.3 读操作建模31-36
• 4.2.4 写操作建模36-41
• 4.3 本章小结41-43
• 第5章 基于AUTOSAR应用建模与分析43-57
• 5.1 AUTOSAR应用抽象43-47
• 5.2 操作系统应用形式化建模47-55
• 5.2.1 os_manager模块建模48-52
• 5.2.2 app_manager模块建模52-54
• 5.2.3 运行过程中各个状态转换过程54-55
• 5.3 本章小结55-57
• 第6章 模型的性质与验证57-65
• 6.1 模型的性质57-61
• 6.1.1 基于AUTOSAR操作系统应用及其状态转换过程的性质57-58
• 6.1.2 基于AUTOSAR存储模块的性质58-61
• 6.2 模型验证61-62
• 6.2.1 基于AUTOSAR操作系统应用及其状态转换过程的验证61-62
• 6.2.2 基于AUTOSAR存储模块的验证62
• 6.3 结果分析62-64
• 6.3.1 应用及其状态转换过程63
• 6.3.2 存储保护机制63-64
• 6.4 本章小结64-65
• 第7章 总结与展望65-67
• 7.1 总结65
• 7.2 展望65-67
• 参考文献67-73
• 附录文中英语简写对照表73-75
• 发表论文和科研情况75-77
• 致谢77

【相似文献】

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

1 邓俊;李红;方正;罗端;胡琦;;AUTOSAR OS存储保护方案的改进与实现[J];仪器仪表学报;2011年09期

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

1 王兆威;基于块设备驱动的安卓系统存储保护技术研究[D];北京理工大学;2015年

2 苏萍;YHFT-XDSP片上二级存储控制器中DMA逻辑的设计与验证[D];国防科学技术大学;2014年

3 何明勇;带存储保护单元的多级片上互连结构设计[D];国防科学技术大学;2014年

4 李青;基于AUTOSAR存储保护机制的形式化建模与分析[D];华东师范大学;2016年

5 燕立明;汽车电子操作系统存储保护机制的设计与实现[D];电子科技大学;2013年

6 姚露;基于DW8051平台的MPU模块设计与验证[D];上海交通大学;2011年

7 唐平;AUTOSAR OS的设计与实现以及向TMS470移植[D];电子科技大学;2012年

，

本文编号：1036103