We propose a novel methodology for validating software product line (PL) models by integrating Statistical Model Checking (SMC) with Process Mining (PM). Our approach focuses on the feature-oriented language QFLan in the PL engineering domain, allowing modeling of PLs with rich cross-tree and quantitative constraints, as well as aspects of dynamic PLs like staged configurations. This richness leads to models with infinite state-space, requiring simulation-based analysis techniques like SMC. For instance, we illustrate with a running example involving infinite state space. SMC involves generating samples of system dynamics to estimate properties such as event probabilities or expected values. On the other hand, PM uses data-driven techniques on execution logs to identify and reason about the underlying execution process. In this paper, we propose, for the first time, applying PM techniques to SMC simulations' byproducts to enhance the utility of SMC analyses. Typically, when SMC results are unexpected, modelers must determine whether they stem from actual system characteristics or model bugs in a black-box manner. We improve on this by using PM to provide a white-box perspective on the observed system dynamics. Samples from SMC are fed into PM tools, producing a compact graphical representation of observed dynamics. The mined PM model is then transformed into a QFLan model, accessible to PL engineers. Using two well-known PL models, we demonstrate the effectiveness and scalability of our methodology in pinpointing issues and suggesting fixes. Additionally, we show its generality by applying it to the security domain.

翻译：我们提出了一种新颖的方法论，通过整合统计模型检测（SMC）与过程挖掘（PM）来验证软件产品线（PL）模型。该方法聚焦于产品线工程领域的功能导向语言QFLan，支持对具有丰富跨树约束与定量约束的PL建模，以及动态PL（如分阶段配置）的建模。这种丰富性导致模型可能具有无限状态空间，需要依赖模拟分析技术（如SMC）。例如，我们通过一个涉及无限状态空间的运行示例加以说明。SMC通过生成系统动态的样本，以估计事件概率或期望值等属性；而PM则利用执行日志的数据驱动技术，识别并推演底层执行过程。本文首次提出将PM技术应用于SMC模拟的副产品，以增强SMC分析的有用性。通常，当SMC结果异常时，建模者必须通过黑盒方式判断问题源自系统实际特性还是模型缺陷。我们通过PM提供系统动态的白盒视角来改进这一过程：将SMC的样本输入PM工具，生成观测动态的紧凑图形化表示，再将其转换为PL工程师可访问的QFLan模型。通过两个经典PL模型，我们展示了该方法在问题定位与修复建议方面的有效性与可扩展性。此外，通过将其应用于安全领域，我们进一步验证了其通用性。