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

Question

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

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

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

Answer 1

Да, я использовал сплав, и это кузены в промышленности. Сплав был наиболее полезен в убеждении меня в том, что мои модели не были дико неправильны или, вернее, показали мне, где они были неправы, и дали глупые результаты. Другие более конкретные инструменты, такие как «Афинская песня» и «Гутман» и «CPSA» Рамсделла, были более полезны в более узких областях. Что еще вы хотели бы услышать?

Answer 2

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

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

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

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

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

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

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

Answer 3

запоздания, добавив к этой теме ... Eunsuk Кан недавно применен сплав для выполнения безопасности анализирует веб-API, для некоторых стартапов (после многих применений сплава в области безопасности, такие как Apurva-х analysis of OAuth и Барт и коллеги analysis of browser based security mechanisms для CSRF и т.д.) ; Памела Зейв работает над системой impressive analysis of Chord, системой однорангового хранения и недавно написала исправление к исходному алгоритму.