针对NAND闪存硬件的形式化建模

发布时间：2018-06-01 09:34

  本文选题：形式化验证 + Coq证明工具　； 参考：《计算机工程》2015年11期

【摘要】：为形式化地验证存储系统中软件的可靠性,引入NAND闪存硬件的形式化模型定义。根据NAND闪存接口标准ONFI,采用形式化语言对NAND闪存硬件的语义进行建模,包括ONFI定义的NAND闪存硬件的存储层次结构、闪存硬件芯片处理命令的内部工作流程、闪存硬件的命令集,以及在此基础之上定义的闪存等基本操作。该NAND闪存形式化模型在定理证明工具Coq中定义实现,其性质在Coq中得到完整证明,可以用于定义和验证基于NAND闪存的存储系统软件。
[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.
【作者单位】： 中国科学技术大学计算机科学与技术学院;中国科学技术大学苏州研究院软件安全实验室;
【基金】：国家自然科学基金青年基金资助项目(61202052,61103023);国家自然科学基金海外及港澳学者合作研究基金资助项目(61229201)
【分类号】：TP333

【参考文献】

相关期刊论文 前1条

1 李胜广;张其善;;闪存设备在嵌入式Linux系统中的应用[J];计算机工程;2007年02期

【共引文献】

相关期刊论文 前4条

1 杨龙婴;郭宇;;针对NAND闪存硬件的形式化建模[J];计算机工程;2015年11期

2 赵军伟;李宏穆;庄阿龙;何剑锋;;NandFLASH和NorFLASH接口设计和驱动开发[J];现代电子技术;2009年14期

3 何志文;郭宝平;;一种智能相机的Bootloader设计与实现[J];微计算机信息;2009年17期

4 毛亮;叶德建;;嵌入式Linux下的闪存自动分区与更新系统[J];计算机应用与软件;2008年11期

【相似文献】

相关期刊论文 前10条

1 汉泽西;吕飞;;大容量NAND Flash在嵌入式系统中的应用[J];石油仪器;2006年01期

2 编辑部;;成长强劲的NAND Flash产业[J];电子与电脑;2006年11期

3 ;NAND一季度表现糟糕[J];电子产品世界;2007年07期

4 江兴;;三星NAND闪存龙头地位牢固[J];半导体信息;2008年03期

5 ;NAND闪存闪现光芒,今年营业收入有望大增[J];今日电子;2013年07期

6 ;云应用导致NAND闪存需求下降[J];电子产品世界;2013年12期

7 羽冬;;东芝推出多芯片封装NAND闪存[J];半导体信息;2004年05期

8 羽冬;;Chip Enable Don't Care的NAND闪存[J];半导体信息;2004年01期

9 任萍;嵌入式NAND Flash稳步起飞[J];电子与电脑;2005年05期

10 马丰玺;杨斌;卫洪春;;非易失存储器NAND Flash及其在嵌入式系统中的应用[J];计算机技术与发展;2007年01期

相关会议论文 前5条

1 ;Design and Implement NAND FLASH Data Storage System Based on the ARM[A];全国数字媒体技术专业建设与人才培养研讨会论文集[C];2011年

2 赵忠文;王魁;;基于NAND Flash的高速大容量固态记录器设计[A];全国第三届信号和智能信息处理与应用学术交流会专刊[C];2009年

3 肖珂;郭永超;郭书军;;基于MTD的NAND Flash驱动开发[A];2010通信理论与技术新发展——第十五届全国青年通信学术会议论文集（上册）[C];2010年

4 雷磊;谢民;李先楚;;基于NAND型Flash的海量存储板的设计与实现[A];全国第二届嵌入式技术联合学术会议论文集[C];2007年

5 刘恕;;NAND Flash的ECC分级及其在ATE设备中的测试方法[A];第五届中国测试学术会议论文集[C];2008年

相关重要报纸文章 前10条

1 佳宜;NAND型Flash缺货恐至2005年[N];电子资讯时报;2004年

2 佳宜;NAND型Flash价跌 需求仍看俏[N];电子资讯时报;2004年

3 燕蕙;休虑NAND型 Flash价跌[N];电子资讯时报;2004年

4 怡均;NAND型Flash难止跌[N];电子资讯时报;2004年

5 ;NAND闪存吃紧[N];计算机世界;2005年

6 周悟;NAND闪存大战在即[N];计算机世界;2005年

7 吴宗翰 DigiTimes 专稿;茂德将于12英寸厂投产NAND Flash[N];电子资讯时报;2006年

8 吴宗翰 DigiTimes;三星、海力士、美光全靠拢NAND Flash[N];电子资讯时报;2006年

9 连于慧/DigiTimes;NAND Flash价格压力沉重 恐再现跌势[N];电子资讯时报;2006年

10 连于慧 DigiTimes;NAND Flash报价跌 厂商大打容量消耗战[N];电子资讯时报;2006年

相关博士学位论文 前5条

1 李江鹏;提高NAND型闪存使用寿命的数字信号处理方法研究[D];上海交通大学;2014年

2 黄敏;提高MLC NAND Flash存储系统可靠性的方法研究[D];哈尔滨工业大学;2016年

3 魏德宝;基于错误特征的NAND Flash存储策略研究[D];哈尔滨工业大学;2016年

4 徐永刚;基于NAND Flash的嵌入式图像记录技术[D];中国科学院研究生院（光电技术研究所）;2013年

5 孙辉;NAND固态盘有限编程/擦除次数的评测模型及优化方法[D];华中科技大学;2014年

相关硕士学位论文 前10条

1 丁德红;嵌入式系统中大页NAND Flash应用研究[D];吉林大学;2008年

2 郑帅;NAND Flash主机接口控制器技术研究[D];华南理工大学;2015年

3 张鹏;NAND Flash坏块管理算法研究与实现[D];哈尔滨工业大学;2015年

4 李雪峰;基于自主CPU的NAND启动的实现[D];北京工业大学;2015年

5 周天伟;NAND闪存的软硬判决纠错码应用研究[D];西安电子科技大学;2014年

6 周仕成;基于NAND FLASH高速海量存储系统的设计[D];上海交通大学;2015年

7 江旭东;基于NAND Flash阵列的高速大容量图像存储器设计[D];中北大学;2016年

8 张云鹏;一种基于虚拟分区页映射的闪存FTL设计[D];安徽大学;2016年

9 张蓉;支持ONFI和Toggle模式的NAND Flash控制器设计[D];华中科技大学;2014年

10 王举利;eMMC存储系统的闪存转换层研究与设计[D];天津工业大学;2016年

，

本文编号：1963713