Cloud computing is a promising concept in the IT evolution that has increasingly attracted attention from both industry and academic sectors. However, it has introduced new security problems and obstacles. Since formal methods provide a reliable mathematical basis giving rise to safely analyzable and easily verifiable models, this paper, the authors propose a formal framework to specify cloud system architectures and verify their inherent proprieties. Bigraphical Reactive Systems are adopted as a semantic framework for their graphical aspect and rigorous basis. They argue that the proposed models are useful for simulation and analysis of cloud systems proprieties as elasticity and plasticity, while using a given model checker tool dedicated to BRS.