Сборники трудов ИСП РАН


Комбинация методов статической верификации композиции требований

В.О. Мордань (ИСП РАН, Москва, Россия)

Аннотация

Статическая верификация программного обеспечения доказывает выполнение требований в программах, однако для этого необходимо большое количество вычислительных ресурсов, кроме того, соответствующая задача не всегда может быть решена. На данный момент не существует универсальный метод статической верификации, который мог бы эффективно проверять произвольные программы, поэтому на практике необходимо выбирать более подходящий метод и настраивать его под конкретную задачу. В данной статье предлагается комбинировать различные методы для повышения производительности и улучшения результата верификации, что можно рассматривать как первый шаг в создании универсального метода статической верификации. Предложенные методы были реализованы для комбинации активно развивающихся в настоящее время методов верификации композиции требований. Апробация реализованных методов на модулях ядра операционной системы Linux продемонстрировала их преимущества относительно отдельного применения методов верификации композиции требований.

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

статическая верификация программного обеспечения; уточнение абстракции по контрпримерам; задача достижимости; композиция требований

Издание

Труды Института системного программирования РАН, том 29, вып. 3, 2017, стр. 151-170.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2017-29(3)-9

Полный текст статьи в формате pdf Вернуться к содержанию тома