Data-driven Formal Modelling and Verification
Model mining is a technique, inspired from process mining, to derive an abstract but concise and functionally structured model from event logs. Such a model is not just a representation of the unfolded behaviour, as in process mining, but comprises, instead, a set of formal rules for generating the system behaviour, thus supporting more powerful predictive capabilities. The set of rules can be either inferred directly from the events logs (constructive mining) or refined by sifting a plausible a priori model using the event logs as a sieve until a reasonably concise model is achieved (refinement mining). We use rewriting logic as the formal framework in which to perform model mining and implement our framework in the FormalMiner tool using the Maude rewrite system. Once the final formal model is attained, it can be used, within the same rewriting logic framework, to predict future evolutions of the behaviour through simulation, to carry out further validation or to analyse properties through model checking.
- Download FormalMiner
Research carried out by Antonio Cerone