Институт системного программирования им. В.П. Иванникова РАН


Повторное использования уточнений для эффективной регрессионной верификации.

Авторы

Д. Бейер, Ш. Лёве, Е. Новиков, А. Стахлбауер, Ф. Вендлер.

Аннотация

Непрерывное тестирование во время разработки является хорошо утвердившейся практикой обеспечения качества программного обеспечения. Непрерывная проверка моделей от ревизии к ревизии еще не утвердилось в качестве стандартной практики, поскольку чрезмерное потребление ресурсов делает ее применение непрактичным. Инструменты проверки моделей вычисляют большое количество фактов, необходимых для верификации программного обеспечения на предмет того, выполняется ли заданная спецификация. Мы выделили группу некоторых промежуточных данных, которые легко хранить и эффективно использовать повторно, – уточнения абстракции. Уточнение абстрактного домена указывает уровень абстракции, на котором производится анализ. Таким образом, уточнения – это ценный результат усилий верификации и было бы нерационально отбрасывать их после каждого запуска верификации. В частности, уточнения достаточно малы, поэтому их легко хранить; кроме того, их легко обрабатывать и они могут оказать большое воздействие на потребление ресурсов. Мы экспериментально показали влияние повторного использования уточнений на примере индустриальных задач, полученных на основе 1119 ревизий 62 драйверов ядра Linux.

Ключевые слова

Формальная верификации, регрессионная проверка.

Издание

Труды 9й объединенной Европейской конференции по программной инженерии и Симпозиума по основам программной инженерии ACM SIGSOFT, страницы 389-399. ACM, New York, 2013.

DOI: 10.1145/2491411.2491429

Научная группа

Технологии программирования

Все публикации за 2013 год Все публикации