FormalMiner: A formal framework for refinement mining

Abstract

Refinement mining has been inspired by process mining techniques and aims to refine an abstract non-deterministic model by sifting it using event logs as a sieve until a reasonably concise model is achieved. FormalMiner is a formal framework that implements model mining using Maude, a modelling language based on rewriting logic. Once the final formal model is attained, it can be used, within the same rewriting-logic framework, to predict the future evolution of the behaviour through simulation, to carry out further validation or to analyse properties through model checking. In this paper we focus on the refinement mining capability of FormalMiner and we illustrate it using a case study from ecology.