一句话：提出 EvoAlloy，将遗传算法引入 Alloy，在保持可靠性的前提下放宽完备性，以扩展可处理规范规模。
形式化方法能精确刻画程序规范并检查系统可靠性，但现有自动化工具（包括 Alloy 等轻量级分析器）在大型真实应用上仍受可扩展性限制，难以广泛采用。本文提出 EvoAlloy，将遗传算法扩展到 Alloy 中：它在 Kodkod 生成的有限关系层面工作，根据失败约束演化染色体，从而在保持可靠性（soundness）的同时放宽完备性（completeness）。可行性研究表明，EvoAlloy 能在传统 Alloy 失败的规范上找到解；虽然小规范耗时更长，但可扩展性使其能处理更大规范。作者设想未来可在小规范上保持可靠且完备，失败时切换到遗传算法。
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.
DOI 原文 ·
@inproceedings{paperbot4695,
title = {An evolutionary approach for analyzing Alloy specifications},
author = {Jianghao Wang and Hamid Bagheri and Myra B. Cohen},
booktitle = {ASE},
year = {2018},
doi = {10.1145/3238147.3240468}
}