A BRS-Based Approach to Model and Verify Cloud Systems Elasticity

Elasticity is actually one major and important asset for cloud-based systems. This property grants this kind of systems the ability to dynamically adjust their resources allocation by scaling up/down when needed in autonomic manner, allowing them to capitalize resource utilization, and maintain a suitable quality of service. In this paper, we lean on formal methods to give a precise and sufficient semantics to cloud system elasticity. We propose a unique semantic framework based on bigraphical reactive systems (BRS) for modeling both structural and behavioral aspects of cloud-based systems. Besides, Maude system serves to simulate and verify the elasticity property inherent to these systems using many model-checking techniques as the model-checking invariants one.