The power of "why" and "why not": enriching scenario exploration with provenance
The power of "why" and "why not": enriching scenario exploration with provenance
复制标题
“为什么”和“为什么不”的力量：通过来源丰富场景探索
DOI：
10.1145/3106237.3106272
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Krishnamurthi, Shriram
中科院分区：
文献类型：
--
作者：
Nelson, Tim;Danas, Natasha;Dougherty, Daniel J.;Krishnamurthi, Shriram
像合金分析器这样的场景发现工具被广泛应用于安全、网络分析、UML分析等众多具体领域。它们可以帮助验证属性，更广泛地说，有助于探索系统的行为。虽然场景查找器因其产生具体示例的能力而有价值，但个别场景仅提供对可能的情况的洞察，让用户就可能需要的内容做出自己的结论。这篇文章通过允许用户问‘’为什么？‘’来丰富场景查找。和‘’有何不可？‘’关于他们所给出的例子的问题。我们将展示如何区分不能一致删除(或更改)的示例部分和仅反映规范中欠约束的部分。在前一种情况下，我们展示了如何确定规范的哪些元素和示例的其他哪些组件一起解释了这些事实的存在。本文将在场景发现中形式化计算来源的行为。我们介绍了Meralgam，这是流行的合金场景查找器的扩展，它实现了这些基础并提供了示例的交互探索。我们还在各种教科书和现实世界的例子中评估了Meralgam的算法。
Scenario-finding tools like the Alloy Analyzer are widely used in numerous concrete domains like security, network analysis, UML analysis, and so on. They can help to verify properties and, more generally, aid in exploring a system's behavior.While scenario finders are valuable for their ability to produce concrete examples, individual scenarios only give insight into what is possible, leaving the user to make their own conclusions about what might be necessary. This paper enriches scenario finding by allowing users to ask ``why?'' and ``why not?'' questions about the examples they are given. We show how to distinguish parts of an example that cannot be consistently removed (or changed) from those that merely reflect underconstraint in the specification. In the former case we show how to determine which elements of the specification and which other components of the example together explain the presence of such facts.This paper formalizes the act of computing provenance in scenario-finding. We present Amalgam, an extension of the popular Alloy scenario-finder, which implements these foundations and provides interactive exploration of examples. We also evaluate Amalgam's algorithmics on a variety of both textbook and real-world examples.
登录
查看更多内容
Mace4 参考手册和指南
DOI：
10.2172/822574
发表时间：
2003
期刊：
ArXiv
影响因子：
--
作者：
W. McCune
通讯作者：
W. McCune
DOI：
10.1007/978-3-642-24485-8_44
发表时间：
2011-10
期刊：
--
影响因子：
--
作者：
S. Maoz;Jan Oliver Ringert;Bernhard Rumpe
通讯作者：
S. Maoz;Jan Oliver Ringert;Bernhard Rumpe
寻找声明性规范的最小不可满足核心
DOI：
--
发表时间：
2008
期刊：
World Congress on Formal Methods
影响因子：
--
作者：
Emina Torlak;F. Chang;D. Jackson
通讯作者：
D. Jackson
验证开放流交换机规格的（不是）好方法：使用合金对开放流交换机进行形式化建模
DOI：
10.1145/2486001.2491711
发表时间：
2013
期刊：
Proceedings of the ACM SIGCOMM 2013 conference on SIGCOMM
影响因子：
--
作者：
Natali Ruchansky;Davide Proserpio
通讯作者：
Davide Proserpio
形式验证中的健全性检查
DOI：
--
发表时间：
2006
期刊：
International Conference on Concurrency Theory
影响因子：
--
作者：
O. Kupferman
通讯作者：
O. Kupferman