本文關鍵詞：基于模型檢測的硬件驗證在金融領域的研究與應用　出處：《湖北工業(yè)大學》2017年碩士論文　論文類型：學位論文

  更多相關文章： 模型檢測 驗證 建模 屬性提取 反例 接觸式圖像傳感控制器

【摘要】：由于功能單一、結構相對簡單,傳統(tǒng)嵌入式控制器只需采用一般的驗證方法即可完全覆蓋產(chǎn)品的功能測試。而主要應用于金融業(yè)的嵌入式外設控制器的設計,則很難沿用原來的驗證方法完全覆蓋產(chǎn)品的功能測試。為此本課題提出結合模型檢測與驗證方法學,對金融領域嵌入式外設控制器進行全覆蓋測試驗證的方法進行研究。本文研究了國內(nèi)外在硬件驗證與模型檢測的現(xiàn)狀和相關技術,包括驗證方法學分析,基于SystemVerilog驗證關鍵技術以及模型檢測硬件驗證相關技術分析;之后對模型檢測建模方法進行研究,其中包括用例模型轉(zhuǎn)化狀態(tài)模型方法研究,狀態(tài)模型轉(zhuǎn)化為nuSMV模型方法及其轉(zhuǎn)換規(guī)則研究;然后又對模型檢測屬性設計方法進行研究,其中包括屬性提取方法研究、屬性分解方法研究,以及屬性設計方法研究;最后進行實例分析,以實際開發(fā)項目A類點鈔機為平臺,對接觸式圖像傳感器控制器進行用例建模、狀態(tài)建模、nuSMV建模,用模型檢測進行驗證并產(chǎn)生反例,通過反例不斷修改接觸式圖像傳感器控制器,最終設計出穩(wěn)定性好的接觸式圖像傳感器控制器。本課題通過使用基于模型檢測的驗證方法完成了接觸式圖像傳感器控制器的設計,解決了項目中接觸式圖像傳感器控制器采集圖像不穩(wěn)定,圖像質(zhì)量差的問題。以后,在硬件設計領域基于模型檢測的驗證方法應用會越來越廣泛。
【學位授予單位】：湖北工業(yè)大學
【學位級別】：碩士
【學位授予年份】：2017
【分類號】：F832;TP273

【參考文獻】

相關期刊論文 前10條

1 黃鎮(zhèn)謹;陳波;歐陽浩;;基于時間策略的連續(xù)時間Markov過程驗證[J];廣西科技大學學報;2014年03期

2 康西楠;施智平;葉世偉;關永;;矩陣變換理論在HOL4中的形式化[J];計算機仿真;2014年03期

3 馬寧;田澤;史嘉濤;趙志強;;AS5643協(xié)議處理FPGA的仿真驗證[J];計算機技術與發(fā)展;2014年05期

4 侯剛;周寬久;勇嘉偉;任龍濤;王小龍;;模型檢測中狀態(tài)爆炸問題研究綜述[J];計算機科學;2013年S1期

5 張玢;;基于PowerPC的H.264編碼核虛擬仿真平臺的構建與應用[J];數(shù)字技術與應用;2013年05期

6 龍士工;王扣武;;多智體系統(tǒng)時序認知規(guī)范的SPIN模型檢測[J];計算機工程與科學;2011年12期

7 邢曉敏;;嵌入式系統(tǒng)的發(fā)展與應用[J];中國水運(下半月);2011年06期

8 李志軍;陳麗娟;劉建霞;張劍飛;;實現(xiàn)SOPC的嵌入式軟硬件協(xié)同設計平臺[J];單片機與嵌入式系統(tǒng)應用;2011年05期

9 李興鋒;張新常;楊美紅;閻保平;;基于SPIN的模塊化模型檢測方法研究[J];電子與信息學報;2011年04期

10 李光亞;;軟件工程若干技術發(fā)展新趨勢[J];微型電腦應用;2010年11期

，

本文編號：1330621