Semantics-Based Analyses for Cloud-Aware Computing

Cloud computing has become a standard IT operational model for ICT infrastructure in industry, due to attractive business drivers: clouds offer elastic resource capacity instead of resource provisioning in advance; clouds also offer the agility to quickly and flexibly deploy new services on the market at a reduced cost. Virtualization is a key technology enabler for cloud computing, which makes elastic amounts of resources available to services; e.g., the processing capacity allocated to a service may be adapted to the demand on the service on the fly. Cloud-aware computing refers to a new way of developing applications for cloud deployment, designed for high availability and elastic scalability on metered resources. Cumulus developed a semantic foundation for techniques to predict the behavior of cloud-aware applications. Cloud-awareness enables the software to negotiate its own quality of service and opens for dynamic and fine-grained resource management. This introduces an element of reflection which goes beyond the state of the art in both formal semantics and static analysis. The project will develop a formal foundation for cloud-aware computing and use this foundation to enable the verification of quantitative assertions about the high-level quality of service and the low-level resource requirements of cloud-aware applications. Cumulus has enabled a shift in the design of virtualized software from model-based simulation and monitoring deployed systems to advanced static analyses which predict worst-case resource requirements early in the software design. The project consisted of three researchers, who developed a fomral calculus to compare cloud-based systems, a tool for resource analysis based on Petri nets, and a proof system for properties of cloud-based systems in the reasoning framework KeY. The project has demonstrated the potential of the approach using semantics-based analysis tools during the design of such applications.

The main goal of Cumulus was to develop a semantic foundation for static analysis techniques for cloud-aware applications. To reach this goal, we developed a calculus named Virtually Timed Ambients with a formal semantics. We showed how different static analysis techniques could be developed based on this semantics, including a compositional technique for type-based resource management and non compositional techniques based on model checking modal formulas expressing relations between response times and resource availability. Furthermore, we devised deductive verification techniques for Real-Time ABS, a richer modelling language for cloud-aware systems, by means of the formal verification system KeY and by hierarchical Petri Net models. During our work, we broadened our international collaboration and worked with researchers at universities in the Netherlans, France, Italy and Spain, as well as on an industrial case study in collaboration with a Dutch company.

Cloud computing is rapidly becoming the default IT operational model adopted in the ICT infrastructure of industry, due to compelling business drivers: clouds offer elastic resource capacity instead of resource provisioning in advance; clouds also offer the agility to quickly and flexibly deploy new services on the market at a reduced cost. Virtualization is a key technology enabler for cloud computing, which makes elastic amounts of resources available to services; e.g., the processing capacity allocated to a service may be adapted to the demand on the service. Cloud-aware computing refers to a new way of developing applications for cloud deployment, designed for high availability and elastic scalability on metered resources. The main goal of Cumulus is to develop a semantic foundation for static analysis techniques for cloud-aware applications. Cloud-awareness enables the software to negotiate its own quality of service and opens for dynamic and fine-grained resource management. This introduces an element of reflection which goes beyond the state of the art in both formal semantics and static analysis. The project will develop a formal foundation for cloud-aware computing and use this foundation to enable the verification of quantitative assertions about the high-level quality of service and low-level resource requirements of cloud-aware applications. The project will develop demonstrators for the approach in terms of semantics-based tools to analyze quantitative assertions for quality of service during the design of such applications. Cumulus will enable a shift in the design of virtualized software from model simulation and monitoring deployed systems to advanced static analyses of worst-case resource requirements early in the software design.