AlloyMax: bringing maximum satisfaction to relational specifications
AlloyMax: bringing maximum satisfaction to relational specifications
复制标题
DOI：
10.1145/3468264.3468587
复制
发表时间：
2021-08
期刊：
影响因子：
--
通讯作者：
Changjian Zhang;Ryan Wagner;Pedro Orvalho;D. Garlan;Vasco M. Manquinho;R. Martins;Eunsuk Kang
中科院分区：
文献类型：
--
作者：
Changjian Zhang;Ryan Wagner;Pedro Orvalho;D. Garlan;Vasco M. Manquinho;R. Martins;Eunsuk Kang
Alloy 是一种基于一阶关系逻辑的声明式建模语言。其基于约束的分析在软件工程中实现了广泛的应用，包括配置综合、错误查找、测试用例生成和安全分析。这些领域中的某些类型的分析任务涉及寻找最佳解决方案。例如，在网络配置问题中，可能需要找到最宽松的配置（即，它允许最大数量的数据包），而不是找到任何有效的配置。然而，由于它依赖于 SAT，Alloy 不能用于指定和分析这些类型的问题。我们提出 AlloyMax，它是 Alloy 的扩展，能够用最佳解决方案表达和分析问题。 AlloyMax 引入了 (1) 少量附加的语言结构，可用于指定涉及最优性的各种问题，以及 (2) 一个新的分析引擎，它利用最大可满足性 (MaxSAT) 求解器来生成最优解决方案。为了实现这种新型分析，我们展示了如何将一阶关系逻辑中的规范转换为 MaxSAT 求解器的输入格式，即加权合取范式 (WCNF) 的布尔公式。我们在问题基准上证明了 AlloyMax 的适用性和可扩展性。据我们所知，AlloyMax 是第一种在关系建模语言中实现最优分析的方法，我们相信 AlloyMax 有潜力为 Alloy 带来广泛的新应用。
Alloy is a declarative modeling language based on a first-order relational logic. Its constraint-based analysis has enabled a wide range of applications in software engineering, including configuration synthesis, bug finding, test-case generation, and security analysis. Certain types of analysis tasks in these domains involve finding an optimal solution. For example, in a network configuration problem, instead of finding any valid configuration, it may be desirable to find one that is most permissive (i.e., it permits a maximum number of packets). Due to its dependence on SAT, however, Alloy cannot be used to specify and analyze these types of problems. We propose AlloyMax, an extension of Alloy with a capability to express and analyze problems with optimal solutions. AlloyMax introduces (1) a small addition of language constructs that can be used to specify a wide range of problems that involve optimality and (2) a new analysis engine that leverages a Maximum Satisfiability (MaxSAT) solver to generate optimal solutions. To enable this new type of analysis, we show how a specification in a first-order relational logic can be translated into an input format of MaxSAT solvers—namely, a Boolean formula in weighted conjunctive normal form (WCNF). We demonstrate the applicability and scalability of AlloyMax on a benchmark of problems. To our knowledge, AlloyMax is the first approach to enable analysis with optimality in a relational modeling language, and we believe that AlloyMax has the potential to bring a wide range of new applications to Alloy.