摘要： 为形式化地验证存储系统中软件的可靠性,引入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
中图分类号:
杨龙婴,郭宇. 针对NAND闪存硬件的形式化建模[J]. 计算机工程.
YANG Longying,GUO Yu. Formal Modeling for NAND Flash Hardware[J]. Computer Engineering.