Model checking and test generation: towards a combined approach to software verification

CímModel checking and test generation: towards a combined approach to software verification
Közlemény típusaConference Paper
Kiadás éve2019
SzerzőkDobos-Kovács, M., and Vörös, A.
SzerkesztőPataki, B.
Konferencia neveProceedings of the 26th PhD Mini-Symposium
Kiadás dátuma01/2019
KiadóBudapest University of Technology and Economics, Department of Measurement and Information Systems
Konferencia helyszíneBudapest, Hungary

Ensuring the correctness of safety-critical systems is a key aspect of the development process. Various approaches exist to find software bugs: (1) model checking examines the mathematical model of the software and proves the logical correctness, while (2) testing is an efficient and practical technique to find bugs. Model checking is a computationally expensive task, as it explores all the possible states of the software, and despite the technological advances of the last decade, software that cannot be formally verified still exists. On the other hand, testing is computationally cheaper than model checking, and widely used by the industry, but providing an efficient test suite for a given program is still under heavy research. The goal of my work is to combine model checking and testing to exploit the advantages of both approaches. I introduce a new algorithm that uses an abstraction-based model checking technique to explore the behavior of the software. In case the model checking algorithm proves the properties of the software, the procedure terminates. If the algorithm can not reach a conclusion, test generation is applied, exploiting the information gathered during state space traversal of model checking.