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

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

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

【參考文獻】

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

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

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

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

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

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

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

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

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

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

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

，

本文編號：1330621