Опыт использования Alloy в реальных проектах
Я был заинтересован в формальных методах в течение некоторого времени. Я использовал формальные методы, чтобы рассуждать о некоторых очень специфических подразделах нескольких проектов, над которыми я работал. Я так и не смог убедить других членов команды попробовать то же самое, не говоря уже о том, чтобы указать весь домен формальным методом.
Один метод, который я нашел особенно интересным, является Alloy. Я думаю, что он может лучше "масштабироваться" как основа для всего проекта, потому что он концептуально и нотационно очень близок к реальным языкам программирования. Кроме того, инструменты достаточно надежны, поэтому преимущества проверки моделей легко доступны.
Мне было бы очень интересно услышать о реальном опыте, который вы, ребята, испытали при использовании Alloy в своих проектах. Считаете ли вы, что это помогло вам в разработке лучшей модели предметной области? Нашли ошибки в модели вашего домена при проверке? Вы бы использовали это снова?
3 ответа
Да, я использовал Alloy, и это кузены в заводских условиях. Сплав помог мне убедить меня в том, что мои модели не были в высшей степени ошибочными, или, скорее, показал мне, где они были не правы, и дал глупые результаты. Другие более специфические инструменты, такие как Афина Сунга и Гутман и CPSA Рамсделла, были более полезны в их более узких областях. О чем еще вы хотели бы услышать?
Я использовал Alloy в нескольких проектах и нашел его полезным; в некоторых, но не во всех этих проектах я смог убедить других использовать также Alloy или, по крайней мере, работать с теми моделями Alloy, которые я написал. Эти проекты могут или не могут быть тем, что вы имеете в виду, когда просите проекты "реального мира", но они, безусловно, имели место в той части реального мира, в которой я работаю.
В 2006 и 2007 годах я создал частичную модель Alloy для текущего проекта спецификации W3C XProc; насколько я могу судить, большинство членов рабочей группы никогда не читали статью, которую я написал (по адресу http://www.w3.org/XML/XProc/2006/12/alloy-models/models.html); они сказали: "О, мы изменили эту часть спецификации на прошлой неделе, так что то, что говорит модель, больше не актуально". Но газете удалось убедить редактора спецификации в том, что абстрактный уровень "компонента", описанный в первом проекте спецификации, был крайне недооценен и должен быть либо полностью определен, либо отброшен. Он отбросил его с (я думаю) хорошими результатами для удобочитаемости и удобства использования спецификации.
В 2010 году я создал модель Alloy для модели данных XPath 1.0, которая выявила некоторые недостатки в спецификации. Реакция большинства заинтересованных сторон (включая рабочую группу W3C, ответственную за поддержку спецификации XPath 1.0), к сожалению, не вызывает оптимизма.
Исследовательский проект, с которым я связан, использовал Alloy для моделирования MLCD Overlap Corpus, коллекции образцов документов и связанной с ними информации, которую мы создаем (гиперссылки подавлены по настоянию SO); Модель Alloy нашла пару ошибок в нашем первоначальном проекте для каталога корпусов, поэтому она того стоила.
И мы также использовали Alloy, чтобы формализовать некоторую работу по моделированию, которую мы проделали над характером транскрипции и расширением различия типа / токена в структуре документа (для нашей статьи, посмотрите материалы 2010 года по Balisage: The Markup Conference). Это лежит немного за пределами обычной области применения Alloy, так как это не имеет ничего общего с разработкой программного обеспечения, но способность Alloy проверять согласованность моделей и генерировать экземпляры неоценима, поскольку показывает нам некоторые логические последствия той или иной возможной аксиомы. для нашей модели.
Чтобы ответить на ваши конкретные вопросы: да, Alloy помог мне определить более чистые модели доменов, и да, он обнаружил ошибки и глюки. Они часто бывают небольшими по причинам, которые Даниэль Джексон объясняет в своей книге " Программные абстракции": во-первых, если вы используете модели во время проектирования, вы обнаруживаете ошибки рано, когда все еще мало. И, во-вторых (по словам Джексона): "Оглядываясь назад, большинство проблем разработки программного обеспечения тривиальны".
Он продолжает: "Но если вы не обращаетесь к ним с глазу на глаз, тривиальные проблемы имеют неприятную привычку становиться нетривиальными". Мой опыт наглядно подтверждает это. Намного лучше, чтобы предотвратить такие проблемы рано. Так что да, я буду использовать Alloy снова.
Запоздало добавляя в эту тему... Eunsuk Kang недавно применил Alloy для анализа безопасности веб-API для некоторых стартапов (после многих применений Alloy в области безопасности, таких как анализ OAuth в Apurva и анализ механизмов безопасности на основе браузера для Barth et al. CSRF и т. Д.); Памела Заве работала над впечатляющим анализом Chord, одноранговой системы хранения, и недавно написала исправление к оригинальному алгоритму.