An evolutionary approach for analyzing Alloy specifications
An evolutionary approach for analyzing Alloy specifications
复制标题
分析合金规格的进化方法
DOI：
10.1145/3238147.3240468
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Cohen, Myra B.
中科院分区：
文献类型：
--
作者：
Wang, Jianghao;Bagheri, Hamid;Cohen, Myra B.
形式化方法使用数学符号和逻辑推理来精确定义程序的规范，从中我们可以实例化系统的有效实例。有了这些技术，我们可以执行多种任务来检查系统的可靠性。尽管存在许多自动化工具，包括那些被认为是轻量级的工具，但它们在实践中仍然缺乏强大的采用。这个问题的关键是可扩展性和对大型真实的应用程序的适用性。在本文中，我们将展示如何放松的完整性保证没有太大的损失，因为健全的维护。我们已经扩展了一个流行的轻量级分析，合金，与遗传算法。我们的新工具EvoAlloy在Kodkod生成的有限关系级别上工作，并根据失败的约束进化染色体。在一项可行性研究中，我们证明了我们可以找到一组超出传统合金失败范围的规范的解决方案。虽然EvoAlloy的小规格需要更长的时间，但可扩展性意味着我们可以处理更大的规格。我们未来的愿景是，当规格很小时，我们可以保持稳健性和完整性，但当这失败时，EvoAlloy可以切换到其遗传算法。
Formal methods use mathematical notations and logical reasoning to precisely define a program's specifications, from which we can instantiate valid instances of a system. With these techniques we can perform a multitude of tasks to check system dependability. Despite the existence of many automated tools including ones considered lightweight, they still lack a strong adoption in practice. At the crux of this problem, is scalability and applicability to large real world applications. In this paper we show how to relax the completeness guarantee without much loss, since soundness is maintained. We have extended a popular lightweight analysis, Alloy, with a genetic algorithm. Our new tool, EvoAlloy, works at the level of finite relations generated by Kodkod and evolves the chromosomes based on the failed constraints. In a feasibility study we demonstrate that we can find solutions to a set of specifications beyond the scope where traditional Alloy fails. While small specifications take longer with EvoAlloy, the scalability means we can handle larger specifications. Our future vision is that when specifications are small we can maintain both soundness and completeness, but when this fails, EvoAlloy can switch to its genetic algorithm.