發(fā)布時(shí)間：2017-10-15 08:30

  本文關(guān)鍵詞：基于AUTOSAR存儲(chǔ)保護(hù)機(jī)制的形式化建模與分析

  更多相關(guān)文章： 形式化建模 模型檢測(cè) 汽車電子規(guī)范 存儲(chǔ)保護(hù)機(jī)制 通信順序進(jìn)程

【摘要】：隨著汽車生產(chǎn)規(guī)模的不斷擴(kuò)大,基于汽車開放系統(tǒng)架構(gòu)AUTOSAR (AUTomotive Open System Architecture)標(biāo)準(zhǔn)也越來越普及。人們對(duì)于基于AUTOSAR規(guī)范的存儲(chǔ)保護(hù)機(jī)制的研究逐步深入,如何才能提高汽車存儲(chǔ)保護(hù)規(guī)范的安全性是當(dāng)下值得研究的問題。本文使用形式化建模語言CSP對(duì)基于AUTOSAR規(guī)范的內(nèi)存保護(hù)機(jī)制以及操作系統(tǒng)應(yīng)用的運(yùn)行機(jī)制進(jìn)行建模。為了驗(yàn)證模型符合AUTOSAR應(yīng)用運(yùn)行機(jī)制中可信應(yīng)用和非可信應(yīng)用調(diào)用系統(tǒng)服務(wù)的規(guī)范、存儲(chǔ)保護(hù)機(jī)制中應(yīng)用、任務(wù)、中斷服務(wù)子例程訪問各個(gè)存儲(chǔ)模塊的規(guī)范,使用線性時(shí)態(tài)邏輯公式(LTL:Linear Temporal Logic)對(duì)描述相關(guān)性質(zhì)并進(jìn)行驗(yàn)證,并使用模型檢測(cè)工具AT(Process Analysis Toolkit)證明模型滿足無死鎖性、安全性、活性等性質(zhì)。運(yùn)用形式化方法對(duì)AUTOSAR存儲(chǔ)保護(hù)機(jī)制建�？梢源_保系統(tǒng)安全性,從邏輯上討論AUTOSAR存儲(chǔ)保護(hù)機(jī)制的正確性對(duì)汽車電子操作系統(tǒng)的安全性提供了可靠支持。
【關(guān)鍵詞】：形式化建模 模型檢測(cè) 汽車電子規(guī)范 存儲(chǔ)保護(hù)機(jī)制 通信順序進(jìn)程
【學(xué)位授予單位】：華東師范大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2016
【分類號(hào)】：U463.6
【目錄】：

• 摘要6-7
• Abstract7-13
• 第1章 緒論13-17
• 1.1 研究的背景13-14
• 1.2 形式化方法14-15
• 1.3 本文的研究?jī)?nèi)容和研究意義15
• 1.3.1 研究?jī)?nèi)容15
• 1.3.2 研究意義15
• 1.4 本文的主要貢獻(xiàn)15-16
• 1.5 本文的組織結(jié)構(gòu)16-17
• 第2章 相關(guān)研究現(xiàn)狀及預(yù)備知識(shí)17-21
• 2.1 國內(nèi)外相關(guān)研究現(xiàn)狀17-18
• 2.2 預(yù)備知識(shí)18-20
• 2.2.1 通信順序進(jìn)程18-19
• 2.2.2 線性時(shí)態(tài)邏輯19
• 2.2.3 PAT工具19-20
• 2.3 本章小結(jié)20-21
• 第3章 總體架構(gòu)和總體建模21-25
• 3.1 研究框架21-23
• 3.1.1 存儲(chǔ)保護(hù)機(jī)制22
• 3.1.2 應(yīng)用及其狀態(tài)轉(zhuǎn)換過程22-23
• 3.2 總體建模23-24
• 3.3 本章小結(jié)24-25
• 第4章 基于AUTOSAR存儲(chǔ)模塊的建模與分析25-43
• 4.1 AUTOSAR OS存儲(chǔ)保護(hù)機(jī)制25-28
• 4.2 AUTOSAR OS存儲(chǔ)形式化建模28-41
• 4.2.1 存儲(chǔ)保護(hù)架構(gòu)28-30
• 4.2.2 存儲(chǔ)模塊建模30-31
• 4.2.3 讀操作建模31-36
• 4.2.4 寫操作建模36-41
• 4.3 本章小結(jié)41-43
• 第5章 基于AUTOSAR應(yīng)用建模與分析43-57
• 5.1 AUTOSAR應(yīng)用抽象43-47
• 5.2 操作系統(tǒng)應(yīng)用形式化建模47-55
• 5.2.1 os_manager模塊建模48-52
• 5.2.2 app_manager模塊建模52-54
• 5.2.3 運(yùn)行過程中各個(gè)狀態(tài)轉(zhuǎn)換過程54-55
• 5.3 本章小結(jié)55-57
• 第6章 模型的性質(zhì)與驗(yàn)證57-65
• 6.1 模型的性質(zhì)57-61
• 6.1.1 基于AUTOSAR操作系統(tǒng)應(yīng)用及其狀態(tài)轉(zhuǎn)換過程的性質(zhì)57-58
• 6.1.2 基于AUTOSAR存儲(chǔ)模塊的性質(zhì)58-61
• 6.2 模型驗(yàn)證61-62
• 6.2.1 基于AUTOSAR操作系統(tǒng)應(yīng)用及其狀態(tài)轉(zhuǎn)換過程的驗(yàn)證61-62
• 6.2.2 基于AUTOSAR存儲(chǔ)模塊的驗(yàn)證62
• 6.3 結(jié)果分析62-64
• 6.3.1 應(yīng)用及其狀態(tài)轉(zhuǎn)換過程63
• 6.3.2 存儲(chǔ)保護(hù)機(jī)制63-64
• 6.4 本章小結(jié)64-65
• 第7章 總結(jié)與展望65-67
• 7.1 總結(jié)65
• 7.2 展望65-67
• 參考文獻(xiàn)67-73
• 附錄文中英語簡(jiǎn)寫對(duì)照表73-75
• 發(fā)表論文和科研情況75-77
• 致謝77

【相似文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前1條

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

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前7條

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 李青;基于AUTOSAR存儲(chǔ)保護(hù)機(jī)制的形式化建模與分析[D];華東師范大學(xué);2016年

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

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

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

，

本文編號(hào)：1036103