Using KLEE to generate test cases for the Texas Instruments® Stellaris® Peripheral Driver Library

Date

2014-08

Authors

Mainor, Fredrick Dean

Journal Title

Journal ISSN

Volume Title

Publisher

Abstract

Software engineers spend much of their time checking the correctness of software. Software testing is the most widely used technique for accomplishing this task. Most of the test cases used for checking software are manually created, and may not always cover all execution paths of the software. If key test cases are not executed, then the possibility of errors within the software still exists. By using tools that can automate the testing of software, software engineers can run exhaustive tests on their applications to provide verification and validation. Symbolic execution is a program analysis technique that can be utilized to achieve this. KLEE is an open-source dynamic test generation tool based on symbolic execution. In this report I present my results from evaluating KLEE on the Texas Instruments® Stellaris® Peripheral Driver Library. The Stellaris® Peripheral Driver Library consists of software drivers for controlling the peripherals on the Stellaris suite of ARM® Cortex-M based microcontrollers. In total 554 functions within the library were tested, and a total of 14763 test cases were generated. There were 32 bugs found in the software, which include assertion violations, memory errors, and arithmetic errors (division by zero, and shift errors).

Description

text

LCSH Subject Headings

Citation