A Framework for Automating Design Level Exploration within the Rodin Toolset
Peter Kovacs (with contributions from Gudmund Grov and Andrew Ireland)
Automated design space exploration in the context of formal modelling is the process of automated generation new models/specifications. This can e.g. be used to fix faulty models, either by abstraction away the mistake or by adaptation/mutation of the model. This report details a tool developed by the first author over the summer of 2014. The tool will act as a framework for future research into this exciting and novel area, targeting the Event-B formalism and the Rodin toolset.