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