Semantics-Based Analyses for Cloud-Aware Computing

Sky-basert programvare har blitt en standard driftsmodell for IKT infrastruktur i industrien på grunn av attraktive forretningsdrivere. I skyen er mengden med tilgjengelige ressurser elastisk i stedet for å være gitt på forhånd. Skyen tilbyr en fleksibilitet som lar oss levere nye tjenester på markedet raskere og til lavere pris. Virtualisering er en viktig muliggjørende teknologi for sky-basert programvare, eller cloud computing, som gjør elastiske mengder med ressurser tilgjengelig. For eksempel kan prosesseringskapasiteten til en tjeneste hele tiden tilpasses tjenestens belastning. Sky-bevisst programvare beskriver en ny måte å utvikle applikasjoner for skyen, der programvaren er designet for høy tilgjengelighet og elastisk skalerbarhet på ressurser med takstameter. Cumulus utviklet et semantisk grunnlag for analyseteknikker som kan forutsi oppførselen til sky-bevisste programmer. Sky-bevissthet lar programvaren forhandle om sin egen tjenestekvalitet og muliggjør dynamisk og finkornet ressursforvaltning. Dette gjør programvaren reflektiv, noe som går utover state-of-the-art i både formell semantikk og statisk analyse. Prosjektet utviklet et formelt grunnlag for sky-bevisst programvare og brukte dette til å verifisere kvantitative påstander om høy-nivå tjenestekvalitet og lavnivå ressursbehov for sky-bevisste programmer. Cumulus har muliggjort en endring i hvordan virtualisert programvare kan utvikles, fra modell-basert simulering og overvåking av utplasserte systemer til avanserte statiske analyser for worst-case ressursbehov tidlig i programvare-designet. Prosjektet har bestått av tre forskere, som utviklet en formell kalkyle for å sammenlikne skybaserte systemer, et verktøy for ressursanalyse basert på Petrinett, og et bevissystem for egenskaper ved skybaserte programmer i resonneringsverktøyet KeY. Prosjektet har demonstrert nytten av den valgte tilnærmingen med semantikk-baserte verktøy under utviklingen av slik programvare.

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.