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