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

TitleModel checking and test generation: towards a combined approach to software verification
Publication TypeConference Paper
Year of Publication2019
AuthorsDobos-Kovács, M., and Vörös, A.
EditorPataki, B.
Conference NameProceedings of the 26th PhD Mini-Symposium
Date Published01/2019
PublisherBudapest University of Technology and Economics, Department of Measurement and Information Systems
Conference LocationBudapest, Hungary
ISBN Number978-963-313-314-9

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.