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


Повторное использования уточнений в CPAchecker.

Авторы

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

Аннотация

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

Издание

Труды конференции по программной инженерии 2014, LNI P-227, страницы 41-42. Köllen Druck + Verlag GmbH, Bonn, 2014.

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

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