Binary Information Press
Software simulation of embedded hardware plays a very significant role when developing embedded software. This paper focuses on the NAND ash K9F1208U0B to build three state transition models and verify its critical specifications using formal methods. The specifications of these three models have been described by computation tree logic, and verified by a tool named VIS. Verification results show that three state transition models are satisfied successfully by the electronic specifications of NAND flash. A software simulator has been implemented based on these three models and delivered a Linux kernel to demonstrate that the Linux kernel runs correctly.