Process Mining meets Statistical Model Checking to Explain Threat Models: Novel Approach to Model Validation and Enhancement (Extended Abstract)

Formal verification of the dynamics of a system can be conducted by employing statistical analysis techniques, such as Statistical Model Checking (SMC). SMC techniques resort to probabilistic simulations to evaluate the system properties to help to circumvent the state space explosion problem, the well-known curse of the classic model checking techniques. Nevertheless, SMC provides only estimations and confidence intervals of the evaluated properties of the system without explaining why the analysis estimated a particular property value. This project aims to present a novel methodology that integrates SMC with process-oriented data-driven techniques known as process mining (PM) applied to threat models. This methodology will empower modelers to see their models’ unfolded behavior instead of just numerical aggregated values obtained by SMC analysis. In the present work, there are two research goals. The primary research goal focus on implementing and validating the novel methodology in which we enrich SMC techniques with PM techniques. The secondary research goals focus on implementing an approach to extract an attack pattern from its textual description and another to extract a textual description of the salient information from the process model discovered using PM techniques. The secondary research goals add the necessary means to assist a modeler in using this novel methodology.