Exploiting model checking for mobile botnet detection