Towards a Formal Model for Cloud Computing Elasticity

Cloud computing is an emerging topic in the IT industry, it brings new design challenges and security issues, as resources rapid availability and quick scalability. Since formal methods provide a reliable mathematical basis giving rise to safely analyzable models, we aim in this paper to propose a formal framework for cloud computing architectural elasticity. Bigraphical Reactive Systems are adopted as a semantic framework for their graphical aspect and rigorous basis. Then, Maude language is used to implement the obtained cloud bigraphical model. Maude system allows us to execute and analyze the formal specification of cloud computing architecture and its elasticity.