Formal verification of a flash memory device driver - An experience report

Moonzoo Kim, Yunja Choi, Yunho Kim, Hotae Kim

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

15 Scopus citations

Abstract

Flash memory has become virtually indispensable in most mobile devices. In order for mobile devices to operate successfully, it is essential that flash memory be controlled correctly through the device driver software. However, as is typical for embedded software, conventional testing methods often fail to detect hidden flaws in the complex device driver software. This deficiency incurs significant development and operation overhead to the manufacturers. In order to compensate for the weaknesses of conventional testing, we have applied NuSMV, Spin, and CBMC to verify the correctness of a multi-sector read operation of the Samsung OneNANDTM flash device driver and studied their relative strengths and weaknesses empirically. Through this project, we verified the correctness of the multi-sector read operation on a small scale. The results demonstrate the feasibility of using model checking techniques to verify the control algorithm of a device driver in an industrial setting.

Original languageEnglish
Title of host publicationModel Checking Software - 15th International SPIN Workshop, Proceedings
Pages144-159
Number of pages16
DOIs
StatePublished - 2008
Event15th International SPIN Workshop on Model Checking of Software, SPIN 2008 - Los Angeles, CA, United States
Duration: 10 Aug 200812 Aug 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5156 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference15th International SPIN Workshop on Model Checking of Software, SPIN 2008
Country/TerritoryUnited States
CityLos Angeles, CA
Period10/08/0812/08/08

Fingerprint

Dive into the research topics of 'Formal verification of a flash memory device driver - An experience report'. Together they form a unique fingerprint.

Cite this