Discovery of SOA Patterns via Model Checking