В данной статье предложен подход
В данной статье предложен подход к интеграции различных методов верификации ПО. Целью его является существенное повышение сложности программных систем, для которых проведение верификации с помощью строгих методов, использующих формальные модели в явном или скрытом виде, сможет давать практически значимые результаты при приемлемых затратах.
Предлагаемый подход основан на объединении нескольких успешно применяемых на практике синтетических методов верификации (расширенный статический анализ, синтетическое структурное тестирование, тестирования на основе моделей и мониторинг формальных свойств) в рамках единой расширяемой среды верификации ПО. В качестве базовой архитектуры для такой среды предложено использовать хорошо зарекомендовавшую себя архитектуру средств тестирования на основе моделей [], расширенную дополнительными компонентами для анализа исходного кода проверяемых компонентов и для различных видов анализа моделей, в том числе разнообразными решателями. Тестирование на основе моделей выбрано основой предложенной архитектуры, поскольку оно является самым сложным видом верификации из объединяемых методов.
Представлен также ряд методических и технических решений, который, по мнению автора, позволит сделать создание описываемой среды верификации практически выполнимым, а кроме того, облегчит ее использование для решения практических задач верификации промышленного ПО.
Еще одной сферой применения такой среды может стать апробация и отладка многочисленных новых техник верификации и анализа свойств ПО, нацеленного на его верификацию, на практически значимых системах разных классов.
