Experience Report: White Box Test Case Generation for Automotive Embedded Software

Testing software based on symbolic execution is a promising and well-researched approach. Recently, various dynamic symbolic execution approaches have been proposed that are of interest for industrial practice. However, the corresponding tools are typically not directly usable on model-based languages that are predominantly used in the automotive sector. To this end, we use an internal software analysis framework for model-based, embedded software that allows us to easily integrate various approaches leveraging static and dynamic symbolic execution. In our case study, we describe idiosyncrasies of automotive embedded software and show the benefits of leveraging symbolic information to generate test cases. We study and compare different techniques for generating test cases. We evaluate all techniques empirically on relevant, real-world programs from engine control.