{Discovery of SOA patterns via model checking}