Unit Testing of Flash Memory Device Driver through a SAT-Based Model Checker

Flash memory has become virtually indispensable in most mobile devices. In order for mobile devices to successfully provide services to users, 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. Model checking techniques have been proposed to compensate weaknesses of conventional testing methods through exhaustive analyses. These techniques, however, require significant manual efforts to create an abstract target model and, thus, are not widely applied in industry. In this project, we applied model checking technique based on Boolean satisfiability (SAT) solver. One advantage of SAT-based model checking is that a target C code can be analyzed directly without an abstract model, thereby enabling fully-a...

• Type: Conference
• Year: 2008
• Where: KBSE
• Authors: Moonzoo Kim, Yunho Kim, Hotae Kim
• Keywords: Conventional Testing Methods, Device Driver, Device Driver Software, KBSE 2008, Software Engineering