Mechanising a formal model of flash memory

被引：11
作者：
Butterfield, Andrew [1 ]
Freitas, Leo [2 ]
Woodcock, Jim [2 ]
机构：
[1] Univ Dublin Trinity Coll, Dublin 2, Ireland
[2] Univ York, York YO10 5DD, N Yorkshire, England
来源：
SCIENCE OF COMPUTER PROGRAMMING | 2009年 / 74卷 / 04期
基金：
英国工程与自然科学研究理事会;
关键词：
Grand challenge; Verification; Flash hardware; Theorem proving; FILE SYSTEM; RELIABILITY;
D O I：
10.1016/j.scico.2008.09.014
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We present second steps in the construction of formal models of NAND flash memory, based oil a recently emerged open standard for such devices. The model is intended as a key part of a pilot project to develop a verified file store system based on flash memory. The project was proposed by Joshi and Holzmann as a contribution to the Grand Challenge in Verified Software, and involves constructing a highly assured flash file store for use in space-flight missions. The model is at a level of abstraction that captures the internal architecture of NAND flash devices. In this paper, we focus Oil mechanising the state model and its initialisation operation, where most of the Conceptual Complexity resides. (C) 2008 Elsevier B.V. All rights reserved.
引用
收藏
页码：219 / 237
页数：19
相关论文
共 32 条
[1]  
ANDY G, 2007, YCS2007423 U YORK DE
[2]  
[Anonymous], 1992, The Z Notation
[3]  
[Anonymous], 2006, OP NAND FLASH INT SP
[4]  
[Anonymous], COMP SOFTW APPL C AN
[5]  
[Anonymous], JFFS JOURNALLING FLA
[6]   RELIABILITY ISSUES OF FLASH MEMORY CELLS [J].
ARITOME, S ;
SHIROTA, R ;
HEMINK, G ;
ENDOH, T ;
MASUOKA, F .
PROCEEDINGS OF THE IEEE, 1993, 81 (05) :776-788
[7]  
Arkoudas K, 2004, LECT NOTES COMPUT SC, V3308, P373
[8]  
BUTTERFIELD A, 2007, 12 IEEE INT C ENG CO
[9]  
FREITAS L, 2007, ONFI SPECIFICATION Z
[10]  
FREITAS L, 2007, CRG12 U YORK
1234