Опыт использования Alloy в реальных проектах

Question

Я уже некоторое время интересуюсь формальными методами.Я использовал формальные методы, чтобы рассуждать о некоторых очень специфических подразделах нескольких проектов, над которыми я работал.Мне так и не удалось убедить других членов команды попробовать то же самое, не говоря уже о том, чтобы указать весь домен с помощью формального метода.

Один из методов, который показался мне особенно интересным, заключается в следующем Сплав.Я думаю, что он может лучше "масштабироваться" в качестве основы для всего проекта, потому что концептуально и нотационно он очень близок к реальным языкам программирования.Кроме того, инструменты достаточно надежны, так что преимущества проверки модели легко доступны.

Мне было бы очень интересно услышать о любом реальном опыте, который у вас, ребята, мог быть при использовании Alloy в ваших проектах.Считаете ли вы, что это помогло вам в разработке лучшей модели предметной области?Были ли обнаружены ошибки в вашей доменной модели во время проверки?Вы бы воспользовались им снова?

Answer 1

Да, я использовал Alloy и его родственников в промышленном отношении.Alloy очень помог мне убедить меня в том, что мои модели не были совершенно неправильными, или, скорее, показал мне, где они были неправильными и приводили к глупым результатам.Другие более конкретные инструменты, такие как Athena Сонга и CPSA Гуттмана и Рамсделла, оказались более полезными в своих более узких областях.О чем еще вы хотели бы услышать?

Answer 2

Я использовал Alloy в нескольких проектах и нашел его полезным;в некоторых, но не во всех этих проектах мне удалось убедить других участников также использовать Alloy или, по крайней мере, работать с моделями Alloy, которые я написал.Эти проекты могут быть или не быть тем, что вы имеете в виду, когда просите о проектах "реального мира", но они, безусловно, имели место в той части реального мира, в которой я работаю.

В 2006 и 2007 годах я создал частичную модель сплава для текущего на тот момент проекта спецификации W3C XProc;насколько я мог судить, большинство членов рабочей группы никогда не читали статью, которую я написал (по адресу http://www.w3.org/XML/XProc/2006/12/alloy-models/models.html);они сказали: "О, мы изменили эту часть спецификации на прошлой неделе, так что то, что говорит модель, больше не актуально".Но статье удалось убедить редактора спецификации в том, что абстрактный уровень "компонента", описанный в первом проекте спецификации, был прискорбно недоопределен и должен быть либо полностью определен, либо исключен.Он отбросил его, что дало (я думаю) хорошие результаты для удобочитаемости и удобства использования спецификации.

В 2010 году я сделал Модель сплава модели данных XPath 1.0, который выявил некоторые сбои в спецификации.Реакция большинства заинтересованных сторон (включая рабочую группу W3C, ответственную за поддержание спецификации XPath 1.0), к сожалению, не была обнадеживающей.

Исследовательский проект, в котором я участвую, использовал Alloy для моделирования корпуса перекрытий MLCD, коллекции образцов документов и связанной с ними информации, которую мы создаем (гиперссылки подавлены по настоянию SO);модель Alloy обнаружила пару ошибок в нашем первоначальном проекте для каталога corpus, так что это стоило затраченных усилий.

И мы также использовали Alloy для формализации некоторой работы по моделированию, которую мы проделали над природой транскрипции и над распространением различия между типом и токеном на структуру документа (для нашей статьи посмотрите труды Бализажа 2010 года:Конференция по разметке).Это немного выходит за рамки обычной области применения Alloy, поскольку не имеет ничего общего с разработкой программного обеспечения, но способность Alloy проверять модели на согласованность и генерировать экземпляры оказалась неоценимой, показав нам некоторые логические следствия той или иной возможной аксиомы для нашей модели.

Чтобы ответить на ваши конкретные вопросы:да, Alloy помог мне указать более чистые модели предметной области, и да, он обнаружил ошибки и глюки.Они часто были маленькими по причинам, которые Дэниел Джексон объясняет в своей книге Программные Абстракции:во-первых, если вы используете модели во время проектирования, вы обнаруживаете ошибки на ранней стадии, когда все все еще маленький.И, во-вторых (по словам Джексона), "оглядываясь назад, большинство проблем при разработке программного обеспечения тривиальны".

Он продолжает:"Но если вы не обращаетесь к ним напрямую, тривиальные проблемы имеют неприятную привычку становиться нетривиальными". Мой опыт наглядно подтверждает это.Гораздо лучше предотвратить такие проблемы пораньше.Так что да, я снова буду использовать Alloy.

Answer 3

С опозданием добавляюсь в эту тему...Ынсук Канг недавно применил Alloy для анализа безопасности веб-API для некоторых стартапов (вслед за многими приложениями Alloy в области безопасности, такими как Apurva анализ OAuth и Барт и др. анализ механизмов безопасности на основе браузера для CSRF и т. д.);Памела Заве работала над впечатляющий анализ Аккорда, одноранговой системы хранения данных, и недавно написала исправление исходного алгоритма.