On October 11th 2018, Johanna Beate Stumpf from the University of Oslo defended her dissertation for the degree of Ph.D. The title of the thesis was “Virtually Timed Ambients: A Calculus for Resource Management in Cloud Computing”. The adjudication committee was Professor Uwe Nestmann (Electrical Engineering and Computer Science, Technische Universität Berlin), Associate Professor Anna Philippou, (Department of Computer Science, University of Cyprus) and Associate Professor Jon Henrik Forssell (Department of Informatics, University of Oslo). Johanna was supervised by Professor Einar Broch Johnsen and Professor Martin Steffen. Her work looked at developing a method of formally modelling analysing the behaviour of processes running on virtual machines running on a cloud computing.
PhD Defence – Johanna B. Stumpf
Cloud computing is a paradigm of distributed computing in which users share resources by storing data and executing processes in common data centres. A key factor for the success of this paradigm is virtualization technology, which represents the resources of an execution environment as a software layer, a so-called virtual machine. Virtualization allows sharing of existing hardware and software resources, improves security by providing isolation of different users who share the same resource, and enables dynamic assignment of resources according to the demands of the user. This sharing of resources creates business drivers which make cloud computing an economically attractive way to deploy software.
Johanna introduces the calculus of virtually timed ambients: a formal model of hierarchical locations for execution with explicit resource provisioning. This calculus is based on the well-known calculus of mobile ambients and is motivated by the use of nested virtualization in cloud computing applications. The investigation of cloud computing from the point of view of process calculi provides a formal specification of the subject, which is necessary in order to develop executable models for analysis and optimization.
The main contributions of the work are the definition of the calculus of virtually timed ambients, and the reasoning about its essential characteristics. In order to enable static analysis, we enhance the calculus with a type system. Furthermore, she defines a modal logic and a corresponding model checker, which is deployed in the definition of resource-awareness of virtually timed ambients, enabling dynamic self-management of processes. Lastly, she presents virtually timed ambients as a framework to analyse virtualization in cloud computing utilizing a prototype implementation. All concepts are illustrated by examples.
