Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

White-box validation of quantitative product lines by statistical model checking and process mining

Roberto Casaluce, Andrea Burattin, Francesca Chiaromonte, Alberto Lluch Lafuente, Andrea Vandin

TL;DR

The paper tackles the challenge of validating complex, infinite-state software product line models by integrating Statistical Model Checking with Process Mining to produce white-box explanations of observed dynamics. It introduces a five-step methodology that converts SMC traces into a mined PM model, which is then transformed back into the modeling language (QFLan) for direct inspection and diff-based refinement. Through three case studies in SPL (Coffee Vending Machine and Elevator) and cyber-security (RisQFLan RobBank), it demonstrates effectiveness, scalability, and cross-domain generality, highlighting how diff models reveal missing or extraneous behaviors and guide fixes. The approach provides a practical, scalable, and domain-general toolchain for model refinement, contributing a principled way to explain and improve behavioral SPL models beyond black-box numerical results.

Abstract

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.

White-box validation of quantitative product lines by statistical model checking and process mining

TL;DR

The paper tackles the challenge of validating complex, infinite-state software product line models by integrating Statistical Model Checking with Process Mining to produce white-box explanations of observed dynamics. It introduces a five-step methodology that converts SMC traces into a mined PM model, which is then transformed back into the modeling language (QFLan) for direct inspection and diff-based refinement. Through three case studies in SPL (Coffee Vending Machine and Elevator) and cyber-security (RisQFLan RobBank), it demonstrates effectiveness, scalability, and cross-domain generality, highlighting how diff models reveal missing or extraneous behaviors and guide fixes. The approach provides a practical, scalable, and domain-general toolchain for model refinement, contributing a principled way to explain and improve behavioral SPL models beyond black-box numerical results.

Abstract

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.
Paper Structure (36 sections, 24 figures, 3 tables)

This paper contains 36 sections, 24 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Synopsis
  3. Further discussion regarding the relationship with 10.1007/978-3-031-25383-6_18
  4. Background
  5. Modeling product lines with QFLan
  6. Black-box analysis of simulation models with Statistical Model Checking
  7. State-of-the-art SMC-based validation process
  8. Synthesis of models from their executions using Process Mining
  9. Method
  10. Model creation
  11. Logs generation
  12. Logs Pre-processing
  13. Process mining
  14. Automatic diff
  15. Experimental evaluation: RQ1 Effectiveness
  16. ...and 21 more sections

Figures (24)

  • Figure 1: Example of the input and output produced by the technique presented in this paper. The input model is simulated with SMC techniques and corresponding traces are used to synthesize a new model which is then compared to the original one and an easy-to-read output is returned to the modeler emphasizing the differences.
  • Figure 2: Feature model for hot beverage vending machines, figure adapted from DBLP:conf/fm/VandinBLL18
  • Figure 3: Action constraints
  • Figure 4: Quantitative constraints
  • Figure 5: Probabilistic process of the model in QFLan
  • ...and 19 more figures