Model-Checking Cloud Systems Using BigMC.
Hamza Sahli, Faïza Belala, Chafia Bouanaka · 2014
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 analysable and easily verifiable models, we aim in this paper to 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. We 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.