计算机工程

• 体系结构与软件技术 • 上一篇    下一篇

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

杨龙婴1,2,郭宇1,2   

  1. (1.中国科学技术大学计算机科学与技术学院,合肥 230026;2.中国科学技术大学苏州研究院软件安全实验室,江苏 苏州 215123)
  • 收稿日期:2014-10-31 出版日期:2015-11-15 发布日期:2015-11-13
  • 作者简介:杨龙婴(1988-),女,硕士研究生,主研方向:形式化验证,软件安全;郭宇,副教授。
  • 基金项目:
    国家自然科学基金青年基金资助项目(61202052,61103023);国家自然科学基金海外及港澳学者合作研究基金资助项目(61229201)。

Formal Modeling for NAND Flash Hardware

YANG Longying  1,2,GUO Yu  1,2   

  1. (1.School of Computer Science and Technology,University of Science and Technology of China,Hefei 230026,China;2.Software Security Laboratory,Suzhou Institute for Advanced Study,University of Science and Technology of China,Suzhou 215123,China)
  • Received:2014-10-31 Online:2015-11-15 Published:2015-11-13

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

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

Abstract: In order to verify the reliability of the software running on storage system formally,a formal model of NAND flash hardware is needed.According to an interface specification named ONFI that is recognized by many companies,a formal model for the semantics of NAND flash hardware is built in formal language.It includes the storage architecture of NAND flash defined by ONFI,the inner workflow of the commands,the command set of the NAND flash and several flash operations defined upon the model.The model is defined in a popular theorem proof assistant,Coq.This model can be used to define and verify the software based on NAND flash storage system.

Key words: formal verification, Coq proof tool, Flash device, formal modeling, high confidence software, storage system

中图分类号: