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


Применимость AutoProof: учебный пример верификации ПО

Мансур Хазеев (Университет Иннополис, Иннополис, респ. Татарстан, Россия)
Виктор Ривера (Университет Иннополис, Иннополис, респ. Татарстан, Россия)
Мануэль Маццара (Университет Иннополис, Иннополис, респ. Татарстан, Россия)
Александр Чичигин (Университет Иннополис, Иннополис, респ. Татарстан, Россия)

Аннотация

Очень часто инструменты статической верификации являются результатом многолетних научно-исследовательских работ. По этой причине разработки ведутся с распределением задач внутри учебных заведений и с расчетом на способность старших исследователей обеспечивать её непрерывность. В такой ситуации некоторые атрибуты качества, такие как удобство и простота использования программного обеспечения, чаще всего, не рассматриваются на должном уровне, что плохо сказывается на возможности дальнейшей коммерциализации продукта. Для того, чтобы данные инструменты получили широкое применение необходимо обратить внимание и направить усилия при дальнейшей доработке на упрощение механизма взаимодействия пользователей с приложением, для того, чтобы дать инженерам программного обеспечения возможность пользоваться инструментом без необходимости полного понимания всех математических механизмов во всех деталях. Для того, чтобы обратить внимание общественности на важность удобства использования инструментов верификации, мы применили инструмент AutoProof к хорошо известному проекту Tokeneer. Данный инструмент использовался для верификации части имплементации реального проекта Tokeneer, в ходе чего были выявлены сильные и слабые стороны AutoProof, и, как результат, был составлен список необходимых улучшений. Результат данной работы иллюстрирует эффективность инструмента при верификации фрагмента реального программного обеспечения: он позволил автоматически проверить практически две трети всех свойств. В то же время, данное исследование показало потребность в доработке документации к данному инструменту и подчеркнуло необходимость улучшения как самого инструмента, так и среды Eiffel IDE.

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

статическая верификация, формальная спецификация, Eiffel, Autoproof, контрактное программирование

Издание

Труды Института системного программирования РАН, том 28, вып. 2, 2016, стр. 111-126.

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

DOI: 10.15514/ISPRAS-2016-28(2)-7

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