Integrating model driven and model checking to mine design patterns