paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A graph solver for the automated generation of consistent domain-specific models

面向一致性领域特定模型自动生成的图求解器
ICSE Proceedings of the 40th International Conference on Software Engineering2018匹配度 3/10 · 论文聚焦于基于图求解器的一致性领域模型自动生成与约束求解,属于建模/形式化方法的邻近方向,可能对测试基准生成有启发;但未涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析,与研究画像的核心交叉点不匹配。引用 53 inbox
Oszkár Semeráth, András Szabolcs Nagy, Dániel Varró
crossref: 2026-09-12

AI 速览

一句话:提出直接在图结构上求解的图求解器,用于自动生成满足元模型与良构约束的大规模一致领域模型。

软件与系统工程中的测试和基准生成常需系统化产生图模型,但自动生成符合元模型并满足工业领域良构约束的一致实例模型十分困难。现有方法将图模型映射为一阶逻辑规约并交由 Alloy 或 Z3 等后端求解,存在严重可扩展性问题。本文提出图求解器框架,直接在图结构上操作,结合部分模型精化、形状分析、增量图查询求值与基于规则的设计空间探索,为一致性模型生成提供更高效引导。在四个领域的初步性能评估表明,该方法可生成比原生 Alloy 映射方法大 1–2 个数量级的模型,规模达 500 至 6000 个对象。

问题
如何自动生成符合元模型并满足所有良构性约束的一致性领域特定图模型,同时避免映射到一阶逻辑求解器导致的可扩展性瓶颈。
方法
提出直接在图结构上运行的图求解器框架,融合部分模型精化、形状分析、增量图查询求值和基于规则的设计空间探索来指导搜索。
评估
在四个领域进行初步性能评估,与原生使用 Alloy 的映射方法相比,生成模型规模大 1–2 个数量级,含 500 到 6000 个对象。
原文摘要(Abstract)

Many testing and benchmarking scenarios in software and systems engineering depend on the systematic generation of graph models. For instance, tool qualification necessitated by safety standards would require a large set of consistent (well-formed or malformed) instance models specific to a domain. However, automatically generating consistent graph models which comply with a metamodel and satisfy all well-formedness constraints of industrial domains is a significant challenge. Existing solutions which map graph models into first-order logic specification to use back-end logic solvers (like Alloy or Z3) have severe scalability issues. In the paper, we propose a graph solver framework for the automated generation of consistent domain-specific instance models which operates directly over graphs by combining advanced techniques such as refinement of partial models, shape analysis, incremental graph query evaluation, and rule-based design space exploration to provide a more efficient guidance. Our initial performance evaluation carried out in four domains demonstrates that our approach is able to generate models which are 1-2 orders of magnitude larger (with 500 to 6000 objects!) compared to mapping-based approaches natively using Alloy.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@inproceedings{paperbot4484,
  title = {A graph solver for the automated generation of consistent domain-specific models},
  author = {Oszkár Semeráth and András Szabolcs Nagy and Dániel Varró},
  booktitle = {ICSE},
  year = {2018},
  doi = {10.1145/3180155.3180186}
}