Formal Specification and Analysis of Cloud Computing Management

Cloud Computing-based systems (i) are safety- and security-critical systems which have strong qualitative and quantitative formal requirements, (ii) have equally important time-critical performance-based quality of service properties (e.g., availability), and (iii) need to dynamically adapt to changes in the potentially hostile (e.g., distributed denial of service attacks) and often probabilistic environment they operate in. These aspects make distributed and Cloud-based systems complex and hard to design, build, test, and verify; and in this context, Cloud Computing management has to deal with a multitude of obstacles for the growth and adoption of the Cloud Computing paradigm. In this thesis, we focus on three of these obstacles: bugs in large distributed systems, service availability, and performance unpredictability. To tackle these challenges and the aforementioned complexity, we propose solutions based on executable formal specifications and formal analysis, using an adequate semantic framework. We chose rewriting logic as the semantic framework and Maude, a language and system based on rewriting logic that offers the possibility of executing and formally analyzing specifications, as the foundation for our work.