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

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

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

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

【相似文獻】

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

1 鄧俊;李紅;方正;羅端;胡琦;;AUTOSAR OS存儲保護方案的改進與實現(xiàn)[J];儀器儀表學報;2011年09期

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

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

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

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

4 李青;基于AUTOSAR存儲保護機制的形式化建模與分析[D];華東師范大學;2016年

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

6 姚露;基于DW8051平臺的MPU模塊設(shè)計與驗證[D];上海交通大學;2011年

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

，

本文編號：1036103