本文選題：形式化驗(yàn)證 + Coq證明工具��； 參考：《計(jì)算機(jī)工程》2015年11期

【摘要】：為形式化地驗(yàn)證存儲(chǔ)系統(tǒng)中軟件的可靠性,引入NAND閃存硬件的形式化模型定義。根據(jù)NAND閃存接口標(biāo)準(zhǔn)ONFI,采用形式化語言對NAND閃存硬件的語義進(jìn)行建模,包括ONFI定義的NAND閃存硬件的存儲(chǔ)層次結(jié)構(gòu)、閃存硬件芯片處理命令的內(nèi)部工作流程、閃存硬件的命令集,以及在此基礎(chǔ)之上定義的閃存等基本操作。該NAND閃存形式化模型在定理證明工具Coq中定義實(shí)現(xiàn),其性質(zhì)在Coq中得到完整證明,可以用于定義和驗(yàn)證基于NAND閃存的存儲(chǔ)系統(tǒng)軟件。
[Abstract]:In order to formally verify the reliability of software in storage system, a formal model definition of NAND flash memory hardware is introduced. According to the NAND flash interface standard ONFI, the semantics of NAND flash memory hardware is modeled by formal language, including the storage hierarchy of NAND flash memory hardware defined by ONFI, the internal workflow of flash memory chip processing commands, and the command set of flash memory hardware. And on the basis of the definition of flash memory and other basic operations. The NAND flash memory formal model is defined and implemented in theorem proving tool Coq. The properties of NAND flash memory are proved in Coq, which can be used to define and validate NAND flash memory based storage system software.
【作者單位】： 中國科學(xué)技術(shù)大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院;中國科學(xué)技術(shù)大學(xué)蘇州研究院軟件安全實(shí)驗(yàn)室;
【基金】：國家自然科學(xué)基金青年基金資助項(xiàng)目(61202052,61103023);國家自然科學(xué)基金海外及港澳學(xué)者合作研究基金資助項(xiàng)目(61229201)
【分類號(hào)】：TP333

【參考文獻(xiàn)】

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

1 李勝廣;張其善;;閃存設(shè)備在嵌入式Linux系統(tǒng)中的應(yīng)用[J];計(jì)算機(jī)工程;2007年02期

【共引文獻(xiàn)】

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

1 楊龍嬰;郭宇;;針對NAND閃存硬件的形式化建模[J];計(jì)算機(jī)工程;2015年11期

2 趙軍偉;李宏穆;莊阿龍;何劍鋒;;NandFLASH和NorFLASH接口設(shè)計(jì)和驅(qū)動(dòng)開發(fā)[J];現(xiàn)代電子技術(shù);2009年14期

3 何志文;郭寶平;;一種智能相機(jī)的Bootloader設(shè)計(jì)與實(shí)現(xiàn)[J];微計(jì)算機(jī)信息;2009年17期

4 毛亮;葉德建;;嵌入式Linux下的閃存自動(dòng)分區(qū)與更新系統(tǒng)[J];計(jì)算機(jī)應(yīng)用與軟件;2008年11期

【相似文獻(xiàn)】

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

1 漢澤西;呂飛;;大容量NAND Flash在嵌入式系統(tǒng)中的應(yīng)用[J];石油儀器;2006年01期

2 編輯部;;成長強(qiáng)勁的NAND Flash產(chǎn)業(yè)[J];電子與電腦;2006年11期

3 ;NAND一季度表現(xiàn)糟糕[J];電子產(chǎn)品世界;2007年07期

4 江興;;三星NAND閃存龍頭地位牢固[J];半導(dǎo)體信息;2008年03期

5 ;NAND閃存閃現(xiàn)光芒,今年?duì)I業(yè)收入有望大增[J];今日電子;2013年07期

6 ;云應(yīng)用導(dǎo)致NAND閃存需求下降[J];電子產(chǎn)品世界;2013年12期

7 羽冬;;東芝推出多芯片封裝NAND閃存[J];半導(dǎo)體信息;2004年05期

8 羽冬;;Chip Enable Don't Care的NAND閃存[J];半導(dǎo)體信息;2004年01期

9 任萍;嵌入式NAND Flash穩(wěn)步起飛[J];電子與電腦;2005年05期

10 馬豐璽;楊斌;衛(wèi)洪春;;非易失存儲(chǔ)器NAND Flash及其在嵌入式系統(tǒng)中的應(yīng)用[J];計(jì)算機(jī)技術(shù)與發(fā)展;2007年01期

相關(guān)會(huì)議論文 前5條

1 ;Design and Implement NAND FLASH Data Storage System Based on the ARM[A];全國數(shù)字媒體技術(shù)專業(yè)建設(shè)與人才培養(yǎng)研討會(huì)論文集[C];2011年

2 趙忠文;王魁;;基于NAND Flash的高速大容量固態(tài)記錄器設(shè)計(jì)[A];全國第三屆信號(hào)和智能信息處理與應(yīng)用學(xué)術(shù)交流會(huì)�？痆C];2009年

3 肖珂;郭永超;郭書軍;;基于MTD的NAND Flash驅(qū)動(dòng)開發(fā)[A];2010通信理論與技術(shù)新發(fā)展——第十五屆全國青年通信學(xué)術(shù)會(huì)議論文集（上冊）[C];2010年

4 雷磊;謝民;李先楚;;基于NAND型Flash的海量存儲(chǔ)板的設(shè)計(jì)與實(shí)現(xiàn)[A];全國第二屆嵌入式技術(shù)聯(lián)合學(xué)術(shù)會(huì)議論文集[C];2007年

5 劉恕;;NAND Flash的ECC分級及其在ATE設(shè)備中的測試方法[A];第五屆中國測試學(xué)術(shù)會(huì)議論文集[C];2008年

相關(guān)重要報(bào)紙文章 前10條

1 佳宜;NAND型Flash缺貨恐至2005年[N];電子資訊時(shí)報(bào);2004年

2 佳宜;NAND型Flash價(jià)跌 需求仍看俏[N];電子資訊時(shí)報(bào);2004年

3 燕蕙;休慮NAND型 Flash價(jià)跌[N];電子資訊時(shí)報(bào);2004年

4 怡均;NAND型Flash難止跌[N];電子資訊時(shí)報(bào);2004年

5 ;NAND閃存吃緊[N];計(jì)算機(jī)世界;2005年

6 周悟;NAND閃存大戰(zhàn)在即[N];計(jì)算機(jī)世界;2005年

7 吳宗翰 DigiTimes 專稿;茂德將于12英寸廠投產(chǎn)NAND Flash[N];電子資訊時(shí)報(bào);2006年

8 吳宗翰 DigiTimes;三星、海力士、美光全靠攏NAND Flash[N];電子資訊時(shí)報(bào);2006年

9 連于慧/DigiTimes;NAND Flash價(jià)格壓力沉重 恐再現(xiàn)跌勢[N];電子資訊時(shí)報(bào);2006年

10 連于慧 DigiTimes;NAND Flash報(bào)價(jià)跌 廠商大打容量消耗戰(zhàn)[N];電子資訊時(shí)報(bào);2006年

相關(guān)博士學(xué)位論文 前5條

1 李江鵬;提高NAND型閃存使用壽命的數(shù)字信號(hào)處理方法研究[D];上海交通大學(xué);2014年

2 黃敏;提高M(jìn)LC NAND Flash存儲(chǔ)系統(tǒng)可靠性的方法研究[D];哈爾濱工業(yè)大學(xué);2016年

3 魏德寶;基于錯(cuò)誤特征的NAND Flash存儲(chǔ)策略研究[D];哈爾濱工業(yè)大學(xué);2016年

4 徐永剛;基于NAND Flash的嵌入式圖像記錄技術(shù)[D];中國科學(xué)院研究生院（光電技術(shù)研究所）;2013年

5 孫輝;NAND固態(tài)盤有限編程/擦除次數(shù)的評測模型及優(yōu)化方法[D];華中科技大學(xué);2014年

相關(guān)碩士學(xué)位論文 前10條

1 丁德紅;嵌入式系統(tǒng)中大頁NAND Flash應(yīng)用研究[D];吉林大學(xué);2008年

2 鄭帥;NAND Flash主機(jī)接口控制器技術(shù)研究[D];華南理工大學(xué);2015年

3 張鵬;NAND Flash壞塊管理算法研究與實(shí)現(xiàn)[D];哈爾濱工業(yè)大學(xué);2015年

4 李雪峰;基于自主CPU的NAND啟動(dòng)的實(shí)現(xiàn)[D];北京工業(yè)大學(xué);2015年

5 周天偉;NAND閃存的軟硬判決糾錯(cuò)碼應(yīng)用研究[D];西安電子科技大學(xué);2014年

6 周仕成;基于NAND FLASH高速海量存儲(chǔ)系統(tǒng)的設(shè)計(jì)[D];上海交通大學(xué);2015年

7 江旭東;基于NAND Flash陣列的高速大容量圖像存儲(chǔ)器設(shè)計(jì)[D];中北大學(xué);2016年

8 張?jiān)迄i;一種基于虛擬分區(qū)頁映射的閃存FTL設(shè)計(jì)[D];安徽大學(xué);2016年

9 張蓉;支持ONFI和Toggle模式的NAND Flash控制器設(shè)計(jì)[D];華中科技大學(xué);2014年

10 王舉利;eMMC存儲(chǔ)系統(tǒng)的閃存轉(zhuǎn)換層研究與設(shè)計(jì)[D];天津工業(yè)大學(xué);2016年

，

本文編號(hào)：1963713