Usability of AutoProof: a case study of software verification

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