SAT-Based Bounded Software Model Checking for Embedded Software: A Case Study

Conventional manual testing often misses corner case bugs in complex embedded software, which can incur large economic loss. To overcome the weakness of manual testing, automated program analysis/testing techniques such as software model checking and concolic testing have been proposed. This paper makes a detailed report on the application of a SAT-based bounded software model checking technique using CBMC to busy box ls which is loaded on a large number of embedded devices such as smart phones and network equipments. In this study, CBMC demonstrated its effectiveness by detecting four bugs of busy box ls, but also showed limitations for the loop analysis. In addition, we report the importance of calculating minimum iterations to exit a loop (MIEL) to prevent false negatives in practice.