【摘要】：傳統(tǒng)汽車標(biāo)準(zhǔn)存儲(chǔ)模塊的安全性較低,汽車電子操作系統(tǒng)在訪問存儲(chǔ)模塊時(shí)會(huì)出現(xiàn)訪問越界和數(shù)據(jù)沖突等問題。為此,提出一種操作系統(tǒng)的存儲(chǔ)保護(hù)機(jī)制。運(yùn)用進(jìn)程代數(shù)給出滿足存儲(chǔ)保護(hù)機(jī)制的形式化驗(yàn)證框架,從邏輯上討論AUTOSAR存儲(chǔ)保護(hù)機(jī)制的重要性,使用進(jìn)程代數(shù)方法對(duì)該機(jī)制建立形式化模型,并根據(jù)AUTOSAR規(guī)范,抽取無死鎖性、安全性、活性等性質(zhì),運(yùn)用模型檢驗(yàn)工具PAT實(shí)現(xiàn)該模型,并對(duì)各個(gè)存儲(chǔ)模塊的讀寫訪問性質(zhì)進(jìn)行驗(yàn)證。仿真結(jié)果表明,與傳統(tǒng)的汽車標(biāo)準(zhǔn)相比,該機(jī)制符合AUTOSAR OS規(guī)范,具有較高的安全性。
[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.
【作者單位】： 華東師范大學(xué)計(jì)算機(jī)科學(xué)與軟件工程學(xué)院;
【基金】：國家自然科學(xué)基金中丹合作項(xiàng)目(6136113600);國家自然科學(xué)基金重點(diǎn)項(xiàng)目(61532019) “核高基”重大專項(xiàng)(2014ZX01038-101-001)
【分類號(hào)】：TP316;TP333;TP309

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 于吉濤;;青花古風(fēng)現(xiàn) 數(shù)據(jù)更安全 aigo H8176S[J];數(shù)碼世界(B版);2009年08期

2 姚露;朱念好;;基于DW8051平臺(tái)的MPU設(shè)計(jì)與驗(yàn)證[J];信息技術(shù);2012年01期

3 鄧俊;李紅;方正;羅端;胡琦;;AUTOSAR OS存儲(chǔ)保護(hù)方案的改進(jìn)與實(shí)現(xiàn)[J];儀器儀表學(xué)報(bào);2011年09期

4 姜徐;蔣志祥;;增強(qiáng)存儲(chǔ)保護(hù)的可信計(jì)算架構(gòu)設(shè)計(jì)[J];計(jì)算機(jī)工程與設(shè)計(jì);2013年09期

5 ;要聞集錦[J];電子與電腦;1995年03期

6 張啟晨;洪俊峰;劉新寧;張萌;;基于ARM7TDMI的TLB組織結(jié)構(gòu)及存儲(chǔ)保護(hù)設(shè)計(jì)[J];電子器件;2008年02期

7 楊先文;李崢;王安;;密碼SoC中數(shù)據(jù)存儲(chǔ)保護(hù)機(jī)制研究與設(shè)計(jì)[J];計(jì)算機(jī)應(yīng)用研究;2011年12期

8 李有志;孫玉方;;Xenix初啟過程分析及漢字化[J];計(jì)算機(jī)研究與發(fā)展;1986年12期

9 立;MacOS 8什么樣?[J];上海微型計(jì)算機(jī);1996年17期

10 雨軒;再塑金身MAC OS 8揭開面紗[J];軟件世界;1997年Z1期

相關(guān)碩士學(xué)位論文 前6條

1 王兆威;基于塊設(shè)備驅(qū)動(dòng)的安卓系統(tǒng)存儲(chǔ)保護(hù)技術(shù)研究[D];北京理工大學(xué);2015年

2 蘇萍;YHFT-XDSP片上二級(jí)存儲(chǔ)控制器中DMA邏輯的設(shè)計(jì)與驗(yàn)證[D];國防科學(xué)技術(shù)大學(xué);2014年

3 何明勇;帶存儲(chǔ)保護(hù)單元的多級(jí)片上互連結(jié)構(gòu)設(shè)計(jì)[D];國防科學(xué)技術(shù)大學(xué);2014年

4 燕立明;汽車電子操作系統(tǒng)存儲(chǔ)保護(hù)機(jī)制的設(shè)計(jì)與實(shí)現(xiàn)[D];電子科技大學(xué);2013年

5 姚露;基于DW8051平臺(tái)的MPU模塊設(shè)計(jì)與驗(yàn)證[D];上海交通大學(xué);2011年

6 唐平;AUTOSAR OS的設(shè)計(jì)與實(shí)現(xiàn)以及向TMS470移植[D];電子科技大學(xué);2012年

，

本文編號(hào)：2134798