Auto-scaling, a key property of cloud computing, allows application owners to acquire and release resourceson demand. However, the shared environment, along with theexponentially large configuration space of available parameters, makes configuration of auto-scaling policies a challenging task. Inparticular, it is difficult to quantify, a priori, the impact of a policyon Quality of Service (QoS) provision. To address this problem, we propose a novel approach based on performance modellingand formal verification to produce performance guaranteeson particular rule-based auto-scaling policies. We demonstratethe usefulness and efficiency of our model through a detailedvalidation process on the Amazon EC2 cloud, using two typesof load patterns. Our experimental results show that it can bevery effective in helping a cloud application owner configure anauto-scaling policy in order to minimise the QoS violations.