Abstract. In this thesis we propose formal verification as a way to produce rigorous performance guarantees for resource control and estimation mechanisms in cloud computing. In particular, with respect to control, we focus on an automated resource provisioning mechanism, commonly referred to as auto-scaling, which allows resources to be acquired and released on demand. However, the shared environment, along with the exponentially large space of available parameters, makes the configuration of auto-scaling policies a challenging task. To address this problem, we propose a novel approach based on performance modelling and formal verification to produce performance guarantees on particular rule-based auto-scaling policies. We demonstrate the usefulness and efficiency of our techniques through a detailed validation process on two public cloud providers, Amazon EC2 and Microsoft Azure, targeting two cloud computing models, Infrastructure as a Service (IaaS) and Platform as a Service (PaaS), respectively.

We then develop novel solutions for the problem of verifying state estimation algorithms, such as the Kalman filter, in the context of cloud computing. To achieve this, we first tackle the broader problem of developing a methodology for verifying properties related to numerical and modelling errors in Kalman filters. This targets more general applications such as automotive and aerospace engineering, where the Kalman filter has been extensively applied. This allows us to develop a general framework for modelling and verifying different filter implementations operating on linear discrete-time stochastic systems, and ultimately tackle the more specific case of cloud computing.