Formal modeling and analysis of resource management for cloud architectures: an industrial case study using Real-Time ABS

We demonstrate by a case study of an industrial distributed system how performance, resource consumption, and deployment on the cloud can be formally modeled and analyzed using the abstract behavioral specification language Real-Time ABS. These non-functional aspects of the system are integrated with an existing formal model of the functional system behavior, achieving a separation of concerns between the functional and non-functional aspects in the integrated model. The resource costs associated with execution in the system depend on the size of local data structures, which evolve over time; we derive corresponding worst-case cost estimations by static analysis techniques and integrate them into our resource-sensitive model. The model is further parameterized with respect to deployment scenarios which capture different application-level management policies for virtualized resources. The model is validated against the existing system’s performance characteristics and used to simulate, analyze, and compare deployment scenarios on the cloud.