ASM-based formal model for analysing cloud auto-scaling mechanisms