本文關(guān)鍵詞：基于UPPAAL平臺的AHB總線形式化驗證方法研究，由筆耕文化傳播整理發(fā)布。

【摘要】：AMBA總線規(guī)范是ARM公司設(shè)計的一種用于高性能嵌入式系統(tǒng)的總線標準。AHB總線是高性能系統(tǒng)總線,它能夠維持外部內(nèi)存帶寬并且可以為CPU連接、片上內(nèi)存和其他直接內(nèi)存訪問(DMA)設(shè)備間的通信提供接口。系統(tǒng)中微小的邏輯錯誤都能導致嚴重的后果,研究并驗證嵌入式系統(tǒng)AHB總線技術(shù)規(guī)范是保障系統(tǒng)安全、快速、高效地運行的重要組成部分。驗證面臨的問題是如何保證在對實時系統(tǒng)一致性建模的前提下對模型做具有完備性驗證,本文采用了形式化的模型驗證技術(shù)。本文首先介紹了AMBA AHB的相關(guān)內(nèi)容,包括AHB總線結(jié)構(gòu)和基于SystemC語言的AHB事務級描述;而后提出了SystemC語言的UPPAAL時間自動機語義;并根據(jù)之前所得到的AHB的SystemC描述,提出了AHB事務級描述到時間自動機模型的轉(zhuǎn)換方法,最后建立了一種利用UPPAAL工具的AHB驗證方案,并給出了部分驗證實例。根據(jù)本文研究進展所示,基于UPPAAL平臺的時間自動機驗證方案,可以有效的驗證AHB總線的各個性能屬性,為AHB的幾個重要性質(zhì)驗證問題提供了一種較好的解決辦法。
【關(guān)鍵詞】：AHB總線 UPPAAL 模型檢測 形式化驗證
【學位授予單位】：廣西民族大學
【學位級別】：碩士
【學位授予年份】：2016
【分類號】：TP336
【目錄】：

• 摘要3-4
• ABSTRACT4-7
• 1 緒論7-12
• 1.1 AMBA介紹7-8
• 1.1.1 AMBA AHB總線簡介7
• 1.1.2 硬件描述語言SystemC簡介7-8
• 1.2 形式化驗證與分析8-9
• 1.2.1 定理證明8-9
• 1.2.2 模型驗證9
• 1.3 時間自動機模型與驗證工具9-10
• 1.3.1 時間自動機簡介9-10
• 1.3.2 驗證工具10
• 1.4 本文的組織結(jié)構(gòu)10-12
• 2 AMBA AHB總線原理與實現(xiàn)12-22
• 2.1 AMBA AHB總線結(jié)構(gòu)與通信原理12-13
• 2.1.1 AHB總線結(jié)構(gòu)分析12-13
• 2.1.2 AMBA AHB通信原理分析13
• 2.2 基于SystemC和TLM2.0的模型構(gòu)建方法13-21
• 2.2.1 事務級建模代碼風格設(shè)計的選擇13-17
• 2.2.2 TLM2.0 的通信機制與數(shù)據(jù)結(jié)構(gòu)17-19
• 2.2.3 AHB總線模型功能及結(jié)構(gòu)設(shè)計19-21
• 2.3 本章小結(jié)21-22
• 3 SYSTEMC的時間自動機語義22-35
• 3.1 SYSTEMC設(shè)計向UPPAAL時間自動機的轉(zhuǎn)化22-29
• 3.1.1 總體結(jié)構(gòu)22-23
• 3.1.2 方法的建模23-24
• 3.1.3 調(diào)度機的建模24-25
• 3.1.4 事件的建模25-27
• 3.1.5 進程和敏感度的建模27-29
• 3.1.6 通道和模塊的建模29
• 3.2 SYSTEMC事務級模型(TLM)到UPPAAL時間自動機的轉(zhuǎn)化29-34
• 3.2.1 限制30-31
• 3.2.2 套接字的轉(zhuǎn)化31
• 3.2.3 非阻塞傳輸機制的轉(zhuǎn)化31-34
• 3.3 本章小結(jié)34-35
• 4 基于時間自動機的形式化驗證方法35-39
• 4.1 基于時間自動機的驗證35-36
• 4.2 時間自動機驗證工具UPPAAL36-39
• 5 AMBA AHB總線模型驗證39-46
• 5.1 基于SYSTEMC語言描述的AHB總線系統(tǒng)的時間自動機模型39-41
• 5.2 BNF與AHB的性質(zhì)刻畫41-43
• 5.2.1 BNF語法介紹41-42
• 5.2.2 AMBA AHB總線性能刻畫42-43
• 5.3 AMBA AHB總線系統(tǒng)的驗證43-45
• 5.4 本章小結(jié)45-46
• 6 總結(jié)與展望46-47
• 6.1 本文總結(jié)46
• 6.2 未來工作46-47
• 參考文獻47-51
• 致謝51-52
• 攻讀碩士期間發(fā)表的學術(shù)論文52

【參考文獻】

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

1 童琨;邊計年;;片上系統(tǒng)設(shè)計中事務級建模技術(shù)綜述[J];計算機輔助設(shè)計與圖形學學報;2007年11期

  本文關(guān)鍵詞：基于UPPAAL平臺的AHB總線形式化驗證方法研究，由筆耕文化傳播整理發(fā)布。

，

本文編號：287507