在实际项目中使用合金的经验

是的,我用过合金,而且它是工业上的表兄弟。合金最有助于让我相信我的模型并没有大错特错——或者更确切地说,它告诉我它们哪里错了,并产生了愚蠢的结果。其他更为具体的工具,如Song的Athena和Guttman以及Ramsdell的CPSA,在其更狭窄的领域中更为有用。你还想知道什么?

我在一些项目中使用了合金,并且发现它很有帮助;在一些但不是所有的项目中,我能够说服其他相关人员也使用合金,或者至少使用我写的合金模型。这些项目可能是,也可能不是你想要的“现实世界”项目,但它们确实发生在我工作的现实世界中。

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 发现了一些规范中的小问题。不幸的是,大多数相关方(包括负责维护XPath1.0规范的W3C工作组)的反应并不令人鼓舞。

我参与的一个研究项目使用了alloy对MLCD重叠语料库建模,我们正在创建的样本文档和相关信息的集合(在SO的坚持下,超链接被抑制);alloy模型在我们最初的语料库目录设计中发现了一些错误,因此非常值得努力。

此外,我们还使用合金形式化了一些我们在转录性质和将类型/标记区分扩展到文档结构方面所做的建模工作(对于我们的论文,请参阅2010年的Balisage会议记录:标记会议)。这有点超出了合金通常的应用领域,因为它与软件设计无关,但是合金检查模型一致性和生成实例的能力对于向我们展示这个或那个可能的模型公理的一些逻辑后果是非常宝贵的。

回答您的具体问题:是的,合金帮助我指定了更清洁的领域模型,是的,它发现了错误和故障。因为丹尼尔·杰克逊在他的书中解释的原因,它们经常很小。 软件抽象 :首先,如果在设计过程中使用模型,则在 一切 仍然很小。第二,用杰克逊的话说,“事后看来,大多数软件设计问题都是微不足道的。”

他继续说:“但是如果你不直接解决这些问题,琐碎的问题会有变得不琐碎的坏习惯。”我的经验充分证实了这一点。最好早点解决这些问题。所以是的,我将再次使用合金。

迟来的添加到这个线程中…Eunsuk Kang最近已经应用合金对一些初创企业的Web API进行了安全分析(继合金在安全方面的许多应用之后,如Apurva's analysis of OAuth 和Barth等人 analysis of browser based security mechanisms 对于CSRF等);Pamela Zave一直在研究 impressive analysis of Chord 是一个对等存储系统,最近编写了对原始算法的修复程序。