TY - GEN
T1 - Formal verification of a flash memory device driver - An experience report
AU - Kim, Moonzoo
AU - Choi, Yunja
AU - Kim, Yunho
AU - Kim, Hotae
PY - 2008
Y1 - 2008
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=54349128722&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-85114-1_12
DO - 10.1007/978-3-540-85114-1_12
M3 - Conference contribution
AN - SCOPUS:54349128722
SN - 3540851135
SN - 9783540851134
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 144
EP - 159
BT - Model Checking Software - 15th International SPIN Workshop, Proceedings
T2 - 15th International SPIN Workshop on Model Checking of Software, SPIN 2008
Y2 - 10 August 2008 through 12 August 2008
ER -