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

摘要：

为形式化地验证存储系统中软件的可靠性,引入NAND闪存硬件的形式化模型定义.根据NAND闪存接口标准ONFI,采用形式化语言对NAND闪存硬件的语义进行建模,包括ONFI定义的NAND闪存硬件的存储层次结构、闪存硬件芯片处理命令的内部工作流程、闪存硬件的命令集,以及在此基础之上定义的闪存等基本操作.该NAND闪存形式化模型在定理证明工具Coq中定义实现,其性质在Coq中得到完整证明,可以用于定义和验证基于NAND闪存的存储系统软件.

关键词：形式化验证、Coq证明工具、闪存设备、形式化建模、高可信软件、存储系统

所属期刊栏目：41

分类号：TP391(计算技术、计算机技术)

资助基金：国家自然科学基金青年基金资助项目61202052,61103023;国家自然科学基金海外及港澳学者合作研究基金资助项目61229201

在线出版日期：2015-12-16（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：94-99