White-Box Validation of Simulated Models using Statistical Model Checking and Process Mining

Simulation-based model validation approaches, such as Statistical Model Checking (SMC), are critical tools for analyzing and optimizing complex systems in diverse domains. Although widely recognized for their effectiveness, traditional SMC techniques primarily provide numerical estimations of a model’s properties and lack behavioral insights. This limitation restricts their ability to highlight any critical issues during model validation. To address these challenges, this doctoral thesis introduces an novel methodology that integrates Process Mining (PM) techniques with SMC, enhancing both the interpretability and reliability of validation processes. The central contribution of this research is the development of the diff model, a graphical tool that systematically identifies discrepancies between formal specifications and observed simulation behaviors. By leveraging PM techniques, the diff model enables the behavioral interpretation of SMC results, facilitating the detection and resolution of unexpected behaviors. In addition to the original, graph-based diff model, we introduce a new version that operates without any procedural graphical representations, broadening its applicability to more frameworks and simulators. The proposed methodology is validated throughout experiments on models from different domains such as Product Line Engineering (PLE), security models, and robotics. Results demonstrate its effectiveness in uncovering hidden issues, improving model reliability, and enabling systematic comparisons between model configurations. This scalability and versatility highlight the potential of the integrated SMC-PM approach to advance simulation-based model validation practices. By integrating SMC with PM techniques, this research addresses the critical limitations of traditional SMC, laying the groundwork for more accurate and interpretable simulation models. The outcomes provide a robust framework for informed decision-making in complex system design, with significant implications for future research and practical applications across various fields.