摘要
为形式化地验证存储系统中软件的可靠性,引入NAND闪存硬件的形式化模型定义。根据NAND闪存接口标准ONFI,采用形式化语言对NAND闪存硬件的语义进行建模,包括ONFI定义的NAND闪存硬件的存储层次结构、闪存硬件芯片处理命令的内部工作流程、闪存硬件的命令集,以及在此基础之上定义的闪存等基本操作。该NAND闪存形式化模型在定理证明工具Coq中定义实现,其性质在Coq中得到完整证明,可以用于定义和验证基于NAND闪存的存储系统软件。
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.
出处
《计算机工程》
CAS
CSCD
北大核心
2015年第11期94-99,共6页
Computer Engineering
基金
国家自然科学基金青年基金资助项目(61202052
61103023)
国家自然科学基金海外及港澳学者合作研究基金资助项目(61229201)
