Automatic Test Cases Generation for C Written Programs Using Model Checking

The present work focuses on the development of a tool that automatically generates coverage criteria based test cases from a C written program. For accomplishing this, the tool translates the C code into PROMELA and generates specifications based on the wanted coverage criteria. Once the model (PROMELA code) and specifications are obtained, it uses SPIN model checker for executing the verification and generating counterexamples which can be used as test cases.