在实际项目中使用 Alloy 的经验
一段时间以来我对形式方法很感兴趣。我使用形式化方法来推理我一直在从事的一些项目的一些非常具体的子领域。我从来没能说服其他团队成员尝试同样的事情，更不用说用正式的方法指定整个域了。
我发现特别有趣的一种方法是合金。我认为它可以更好地“扩展”作为整个项目的基础，因为它在概念上和符号上都非常接近实际的编程语言。此外，这些工具非常可靠，因此可以轻松获得模型验证的好处。
我非常有兴趣了解你们在项目中使用合金的实际经验。您认为它对您设计更好的领域模型有帮助吗？验证过程中是否发现域模型存在错误？你会再次使用它吗？
I have been interested in formal methods for some time. I have used formal methods to reason about some very specific sub-areas of a few projects I have been working on. I was never able to convince other team members to try the same let alone specify an entire domain with a formal method.
One method I have found particularly interesting is Alloy. I think that it may "scale" better as foundation for an entire project because it is conceptually and notationally very close to actual programming languages. Furthermore, the tools are quite solid so that the benefits of model verification are readily available.
I'd be very much interested to hear about any real-world experiences you folks might have had with using Alloy in your projects. Do you feel that it has helped you in designing a better domain model? Did find errors in your domain model during verification? Would you use it again?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（3）
我在一些项目中使用了 Alloy，并发现它很有帮助；在一些但不是全部的项目中，我已经能够说服其他相关人员也使用 Alloy，或者至少使用我编写的 Alloy 模型。这些项目可能是也可能不是您要求的“现实世界”项目，但它们肯定发生在我工作的现实世界的一部分中。
在 2006 年和 2007 年，我为当时的 W3C XProc 规范草案；据我所知，工作组的大多数成员从未阅读过我写的论文（位于 http://www.w3.org/XML/XProc/2006/12/alloy-models/models.html);他们说“哦，我们上周改变了规范的这一部分，所以模型所说的不再相关”。但该论文确实成功说服了规范的编辑，规范初稿中描述的抽象“组件”级别严重不足，需要完全指定或删除。他放弃了它，（我认为）规范的可读性和可用性取得了良好的结果。
2010 年，我制作了一个 XPath 1.0 数据模型的合金模型，它发现了规范中的一些问题。不幸的是，大多数感兴趣的各方（包括负责维护 XPath 1.0 规范的 W3C 工作组）的反应并不令人鼓舞。
我参与的一个研究项目使用 Alloy 对 MLCD Overlap Corpus 进行建模，这是我们正在创建的示例文档和相关信息的集合（在 SO 的坚持下抑制了超链接）； Alloy 模型在我们语料库目录的初始设计中发现了一些错误，因此这是非常值得的。
我们还使用 Alloy 来形式化我们在转录本质以及将类型/标记区别扩展到文档结构方面所做的一些建模工作（对于我们的论文，请查找 Balisage 的 2010 年会议记录：标记会议）。这有点超出了 Alloy 的通常应用领域，因为它与软件设计无关，但是 Alloy 检查模型一致性和生成实例的能力对于向我们展示这个或那个可能的公理的一些逻辑结果是非常宝贵的。对于我们的模型。
回答您的具体问题：是的，Alloy 帮助我指定了更清晰的域模型，是的，它发现了错误和故障。它们通常都很小，原因是 Daniel Jackson 在他的《软件抽象》一书中解释了这一点：首先，如果您在设计过程中使用模型，那么当一切都还处于静止状态时，您就会及早发现错误。小的。其次（用杰克逊的话说），“事后看来，大多数软件设计问题都是微不足道的。”
他继续说道：“但如果你不正面解决这些问题，琐碎的问题就会变得不平凡。”我的经历充分证实了这一点。最好尽早阻止此类问题。所以是的，我会再次使用合金。
I've used Alloy on a few projects and have found it helpful; on some but not all of those projects I have been able to persuade others involved to use Alloy as well, or at least to work with the Alloy models I wrote. These projects may or may not be what you have in mind in asking for 'real-world' projects, but they certainly took place in the part of the real world I work in.
In 2006 and 2007 I created a partial Alloy model for the then-current draft of the W3C XProc specification; as far as I could tell, most members of the working group never read the paper I wrote (at http://www.w3.org/XML/XProc/2006/12/alloy-models/models.html); they said "Oh, we changed that part of the spec last week, so what the model says is no longer relevant". But the paper did manage to persuade the editor of the spec that the abstract 'component' level described in the first draft of the spec was woefully underspecified and needed to be either fully specified or dropped. He dropped it, with (I think) good results for the readability and usability of the spec.
In 2010 I made an Alloy model of the XPath 1.0 data model, which uncovered some glitches in the specification. The reaction of most interested parties (including the W3C working group responsible for maintaining the XPath 1.0 spec) has, unfortunately, not been encouraging.
A research project I'm involved with has used Alloy to model the MLCD Overlap Corpus, a collection of sample documents and related information we are creating (hyperlinks suppressed at SO's insistence); the Alloy model found a couple of errors in our initial design for the corpus catalog, so it was well worth the effort.
And we have also used Alloy to formalize some modeling work we have done on the nature of transcription and on the extension of the type/token distinction to document structure (for our paper, look for the 2010 proceedings of Balisage: The Markup Conference). This lies a little bit outside Alloy's usual area of application, as it has nothing to do with software design, but Alloy's ability to check models for consistency and generate instances has been invaluable in showing us some of the logical consequences of this or that possible axiom for our model.
To answer your specific questions: yes, Alloy has helped me specify cleaner domain models, and yes, it has found errors and glitches. They have often been small, for the reasons Daniel Jackson explains in his book Software Abstractions: first, if you use models during design, you catch errors early, when everything is still small. And, second (in Jackson's words), "In hindsight, most software design issues are trivial."
He continues: "But if you don't address them head-on, trivial issues have a nasty habit of becoming nontrivial." My experience amply confirms this. Much better to head off such problems early. So yes, I will use Alloy again.
是的，我在工业上使用过合金及其近亲。 Alloy 最有帮助的是让我相信我的模型并没有大错特错，或者更确切地说，它向我展示了它们错在哪里并导致了愚蠢的结果。其他更具体的工具，如 Song 的 Athena 和 Guttman 以及 Ramsdell 的 CPSA 在其较小的领域中更有用。您还想听什么？
Yes, I've used Alloy and it's cousins industrially. Alloy has been most helpful in convincing me that my models weren't wildly wrong---or rather, showing me where they were wrong and gave rise to silly results. Other more specific tools, like Song's Athena and Guttman and Ramsdell's CPSA have been more useful in their narrower domains. What more would you like to hear about?
迟来的添加到这个线程... Eunsuk Kang 最近应用 Alloy 为一些初创公司执行 Web API 的安全分析（遵循 Alloy 在安全方面的许多应用，例如 Apurva 的 OAuth 分析 和 Barth 等人的 基于浏览器的 CSRF 安全机制分析）； Pamela Zave 一直致力于对 Chord 进行令人印象深刻的分析，这是一个对等网络存储系统，并且最近编写了对原始算法的修复。
Belatedly adding to this thread... Eunsuk Kang has recently applied Alloy to perform security analyses of web APIs for some start ups (following many applications of Alloy in security such as Apurva's analysis of OAuth and Barth et al's analysis of browser based security mechanisms for CSRF etc); Pamela Zave has been working on an impressive analysis of Chord, a peer to peer storage system, and has recently written up a fix to the original algorithm.