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

• URL: http://arxiv.org/abs/2401.13019v1
• Date: Tue, 23 Jan 2024 17:27:13 GMT
• Title: White-box validation of quantitative product lines by statistical model checking and process mining
• Authors: Roberto Casaluce, Andrea Burattin, Francesca Chiaromonte, Alberto Lluch Lafuente, Andrea Vandin
• Abstract summary: 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.
• Score: 1.0918484507642576
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• EMR-Merging: Tuning-Free High-Performance Model Merging [55.03509900949149]
  We show that Elect, Mask & Rescale-Merging (EMR-Merging) shows outstanding performance compared to existing merging methods. EMR-Merging is tuning-free, thus requiring no data availability or any additional training while showing impressive performance.
  arXiv  Detail & Related papers  (2024-05-23T05:25:45Z)
• OSM: Leveraging Model Checking for Observing Dynamic 1 behaviors in Aspect-Oriented Applications [0.0]
  observe-based statistical model-checking (OSM) framework devised to craft executable formal models directly from foundational system code. This ensures the unyielding performance of electronic health record systems amidst shifting preconditions.
  arXiv  Detail & Related papers  (2024-03-03T00:03:34Z)
• Online Variational Sequential Monte Carlo [49.97673761305336]
  We build upon the variational sequential Monte Carlo (VSMC) method, which provides computationally efficient and accurate model parameter estimation and Bayesian latent-state inference. Online VSMC is capable of performing efficiently, entirely on-the-fly, both parameter estimation and particle proposal adaptation.
  arXiv  Detail & Related papers  (2023-12-19T21:45:38Z)
• Simplifying Complex Observation Models in Continuous POMDP Planning with Probabilistic Guarantees and Practice [9.444784653236157]
  We deal with the question of what would be the implication of using simplified observation models for planning. Our main contribution is a novel probabilistic bound based on a statistical total variation distance of the simplified model. Our calculations can be separated into offline and online parts, and we arrive at formal guarantees without having to access the costly model at all during planning.
  arXiv  Detail & Related papers  (2023-11-13T20:55:02Z)
• QualEval: Qualitative Evaluation for Model Improvement [82.73561470966658]
  We propose QualEval, which augments quantitative scalar metrics with automated qualitative evaluation as a vehicle for model improvement. QualEval uses a powerful LLM reasoner and our novel flexible linear programming solver to generate human-readable insights. We demonstrate that leveraging its insights, for example, improves the absolute performance of the Llama 2 model by up to 15% points relative.
  arXiv  Detail & Related papers  (2023-11-06T00:21:44Z)
• Predictable MDP Abstraction for Unsupervised Model-Based RL [93.91375268580806]
  We propose predictable MDP abstraction (PMA) Instead of training a predictive model on the original MDP, we train a model on a transformed MDP with a learned action space. We theoretically analyze PMA and empirically demonstrate that PMA leads to significant improvements over prior unsupervised model-based RL approaches.
  arXiv  Detail & Related papers  (2023-02-08T07:37:51Z)
• Automatically Marginalized MCMC in Probabilistic Programming [12.421267523795114]
  Hamiltonian Monte Carlo (HMC) is a powerful algorithm to sample latent variables from Bayesian models. We propose to use automatic marginalization as part of the sampling process using HMC in a graphical model extracted from a PPL.
  arXiv  Detail & Related papers  (2023-02-01T16:34:07Z)
• CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version) [62.96267257163426]
  We introduce the CoCoMoT (Computing Conformance Modulo Theories) framework. First, we show how SAT-based encodings studied in the pure control-flow setting can be lifted to our data-aware case. Second, we introduce a novel preprocessing technique based on a notion of property-preserving clustering.
  arXiv  Detail & Related papers  (2021-03-18T20:22:50Z)
• Nonintrusive Uncertainty Quantification for automotive crash problems with VPS/Pamcrash [0.0]
  surrogate models (metamodels) allow drastically reducing the computational cost of Monte Carlo process. kernel Principal Component Analysis (kPCA) is found to be effective to simplify the model outcome description. A benchmark crash test is used to show the efficiency of combining metamodels with kPCA.
  arXiv  Detail & Related papers  (2021-02-15T16:59:39Z)
• Goal-Conditioned End-to-End Visuomotor Control for Versatile Skill Primitives [89.34229413345541]
  We propose a conditioning scheme which avoids pitfalls by learning the controller and its conditioning in an end-to-end manner. Our model predicts complex action sequences based directly on a dynamic image representation of the robot motion. We report significant improvements in task success over representative MPC and IL baselines.
  arXiv  Detail & Related papers  (2020-03-19T15:04:37Z)
• Markov-Chain Monte Carlo Approximation of the Ideal Observer using Generative Adversarial Networks [14.792685152780795]
  The Ideal Observer (IO) performance has been advocated when optimizing medical imaging systems for signal detection tasks. To approximate the IO test statistic, sampling-based methods that employ Markov-Chain Monte Carlo (MCMC) techniques have been developed. Deep learning methods that employ generative adversarial networks (GANs) hold great promise to learn object models from image data.
  arXiv  Detail & Related papers  (2020-01-26T21:51:08Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.