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

• 作者: 杨龙婴 郭宇
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 形式化验证 Coq证明工具 闪存设备 形式化建模 高可信软件 存储系统
• 年，卷（期）: 2015,（11）
• 所属期刊栏目: 体系结构与软件技术
• 页码范围: 94-99
• 页数: 6页
• 分类号: TP391
• 字数: 5422字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2015.11.017

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	郭宇	中国科学技术大学计算机科学与技术学院	12	38	3.0	6.0
5	杨龙婴	中国科学技术大学计算机科学与技术学院	1	3	1.0	1.0