AUTOSAR OS存储保护机制的形式化验证框架

发布时间：2018-07-20 21:14

【摘要】：传统汽车标准存储模块的安全性较低,汽车电子操作系统在访问存储模块时会出现访问越界和数据冲突等问题。为此,提出一种操作系统的存储保护机制。运用进程代数给出满足存储保护机制的形式化验证框架,从逻辑上讨论AUTOSAR存储保护机制的重要性,使用进程代数方法对该机制建立形式化模型,并根据AUTOSAR规范,抽取无死锁性、安全性、活性等性质,运用模型检验工具PAT实现该模型,并对各个存储模块的读写访问性质进行验证。仿真结果表明,与传统的汽车标准相比,该机制符合AUTOSAR OS规范,具有较高的安全性。
[Abstract]:The security of the traditional automobile standard storage module is low, and the problems of accessing the storage module and data conflict will occur in the automotive electronic operating system. Therefore, a storage protection mechanism of the operating system is proposed. The formal verification framework satisfying storage protection mechanism is given by using process algebra. The importance of AUTOSAR storage protection mechanism is discussed logically. The formal model of this mechanism is established by using process algebra method, and the deadlock-free property is extracted according to AUTOSAR specification. The model is implemented by using Pat, a model checking tool, and the read / write access properties of each storage module are verified. The simulation results show that compared with the traditional automotive standards, the proposed mechanism conforms to AUTOSAR OS specification and has higher security.
【作者单位】： 华东师范大学计算机科学与软件工程学院;
【基金】：国家自然科学基金中丹合作项目(6136113600);国家自然科学基金重点项目(61532019) “核高基”重大专项(2014ZX01038-101-001)
【分类号】：TP316;TP333;TP309

【相似文献】

相关期刊论文 前10条

1 于吉涛;;青花古风现 数据更安全 aigo H8176S[J];数码世界(B版);2009年08期

2 姚露;朱念好;;基于DW8051平台的MPU设计与验证[J];信息技术;2012年01期

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

4 姜徐;蒋志祥;;增强存储保护的可信计算架构设计[J];计算机工程与设计;2013年09期

5 ;要闻集锦[J];电子与电脑;1995年03期

6 张启晨;洪俊峰;刘新宁;张萌;;基于ARM7TDMI的TLB组织结构及存储保护设计[J];电子器件;2008年02期

7 杨先文;李峥;王安;;密码SoC中数据存储保护机制研究与设计[J];计算机应用研究;2011年12期

8 李有志;孙玉方;;Xenix初启过程分析及汉字化[J];计算机研究与发展;1986年12期

9 立;MacOS 8什么样?[J];上海微型计算机;1996年17期

10 雨轩;再塑金身MAC OS 8揭开面纱[J];软件世界;1997年Z1期

相关硕士学位论文 前6条

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

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

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

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

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

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

，

本文编号：2134798