Использование метода ограниченной проверки моделей для генерации тестов

В настоящее время автоматическая генерация тестов исследуется всё более и более активно, поскольку является решением многих проблем, связанных с тестированием программного обеспечния (ПО), таких как необходимость написания тестов и обеспечения тестового покрытия с учётом человеческого фактора.
Наиболее перспективным методом автоматической генерации тестов является динамическое символьное исполнение (dynamic symbolic execution, DSE), выполняемое с помощью автоматического решателя ограничений, например SMT-решателя. Данный метод во многом похож на метод ограниченной проверки моделей, который также предполагает построение моделей из исходного кода, проверку логических свойств на них и обработку полученной модели.
В данной работе рассматривается метод генерации модульных тестов для языка C, основанный на методе ограниченной проверки моделей. Показано, что эти методы имеют много общего и могут быть реализованы с использованием общих базовых компонентов. Реализован прототип средства генерации тестов, основанный на работающем средстве ограниченной проверки моделей Borealis.
Прототип средства был опробован на множестве примеров и показал хорошие результаты с точки зрения полноты тестового покрытия и избыточности тестового набора.