Abstract: In current information age, flash memory becomes daily goods for virtually all electrical consumer devices such as mobile phone, digital camera, etc. For such devices to provide services to users successfully, it is essential that flash memory should be controlled correctly through its device driver software. However, as typical for embedded software, conventional testings easily fail to detect hidden flaws in the complex device driver software. That deficiency incurs significant development and operation overhead to the manufacturers.

In order to compensate the weakness of conventional testings, we have applied several formal verification tools to analyze the OneNAND device driver software. Our goal was to investigate how formal verification techniques can alleviate debugging effort practically. Therefore, we focused to utilized off-the-shelf formal verification tools and apply them strategically by assigning multiple tools with their most appropriate verification tasks. Through the project, we obtained several interesting analysis results.

Moonzoo Kim received the Ph.D. degree in computer and information science from the University of Pennsylvania, Philadelphia, in 2001. After working as a Research Engineer at Samsung SECUi.COM and Pohang University of Science and Technology, he joined the faculty of the Korea Advanced Institute of Science and Technology, Daejeon, in 2006. He currently focuses on developing provable software in the domain of embedded systems by using model checking and runtime verification techniques. His research interests include the specification and analysis of embedded systems, automated software engineering tools, and formal methods. Appointments: dcm@cs.cmu.edu