Геймификация верификации через краудсорсинг

Пользователи, участвующие в программе DARPA, безвозмездно сгенерировали сотни тысяч комментариев к программному коду 15 Июнь 2015, 07:45

Итоги первого этапа программы DARPA, в ходе реализации которой для ускорения верификации систем программного обеспечения (software system) использовались публично доступные онлайн-игры — команда Crowd Sourced Formal Verification (CSFV) получила сотни тысяч комментариев. Подобные результаты подтвердили идею о том, что онлайн-игры могут стать эффективным средством коллективного решения проблем, связанных с ПО. Результаты вдохновили DARPA на старт нового этапа программы игры, во время проведения которого планируется не только «закрепить успех», но и узнать больше о нераскрытом потенциале такого подхода.

«Мы довольны результатами и собираемся заинтересовать пользователей нашими новыми играми, которые можно будет опробовать в течение нескольких недель — посмотрим, что еще интересного есть в этой идее, — рассказывает руководитель программы Майкл Се (Michael Hsieh). — Системы программного обеспечения в последнее десятилетие развивались быстрее, чем методы их верификации. И сегодня просто не хватает экспертов, которое могли бы провести «ручной» анализ в масштабах, требуемых для проведения формальной верификации бесчисленных систем ПО, которые запускаются каждый день».

Использование ненадежного софта означает внушительные расходы на государственном и глобальном уровнях. Существующие на сегодня подходы к разработке приводят к тому, что ПО содержит от 1 до 5 ошибок на каждую тысячу строк программного кода. Формальная верификация — математический метод подтверждения общего соответствия кода определенным требованиям — лучший способ увериться в том, что данный фрагмент ПО не содержит определенного типа ошибок. Но сегодня формальная верификации почти всегда выполняется вручную специально обученными инженерами. К тому же, стоимость этого метода оправдана лишь в случае работы с небольшими особо важными компонентами ПО.

В декабре 2013 года DARPA в рамках программы CSFV запустила первую версию веб-портала Verigames, на котором было размещено пять бесплатных онлайн-игр, использующих метод формальной верификации. Алгоритмы, использованные в этих играх, переводили действия игроков в программные комментарии и помогали экспертам в области формальной верификации сгенерировать математические доказательства для верификации отсутствия ошибок в программном обеспечении, написанном с использованием языков программирования «Си» и Java. В ходе анализа результатов обнаружилось, что не-эксперты, игравшие в игры на веб-портале, параллельно создали сотни тысяч комментариев.

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

  • Dynamakr: Игрокам необходимо активировать секретный узор в космической головоломке;

  • Paradox: Игроку предлагается, используя набор инструментов, оптимизировать обширные сети;

  • Ghost Map Hyperspace: Необходимо сразиться с инопланетянами и попытаться закрыть их гиперпространственный туннель;

  • Monster Proof: Игрокам предлагается исследовать царство монстров и разгадывать головоломки для набора очков;

  • Binary Fission: Игра для любителей расщеплять атомы, в которой необходимо смешивать и сравнивать кварки.