Designing Resource-Aware Applications for the Cloud using Formal Methods

Einar Broch Johnsen

Department of Informatics,
University of Oslo, Norway

Abstract

Deployment on the cloud gives software designers far reaching control over the resource parameters of the execution environment, such as the number and kind of processors, the amount of memory and storage capacity, and the bandwidth. In this context, designers can also control their software’s trade-offs between the incurred cost and the delivered quality-of-service. Resource-aware services, which are designed for scalability, can even change these parameters dynamically, at runtime, to meet their service-level agreements. But how can we ensure that we made good design decisions for such services, before they are actually deployed? In this talk, we discuss how semantics and formal methods can be used to model and reason about resource-aware services and their service contracts, illustrated by work on executable modelling and analysis of virtualized services in the EU project Envisage.

Short bio

Einar Broch Johnsen http://einarj.at.ifi.uio.no/ is a professor at the Department of Informatics, University of Oslo. His research interests include programming models and methodology; program specification and modeling; formal methods and associated theory; lightweight analysis, type systems, testing; as well as deductive verification and formal logic. He is active in formal methods for distributed and concurrent systems, including object-oriented and concurrent languages, manycore computing, and cloud computing. He is one of the main developers of the ABS modeling language and the coordinator of the EU FP7 project Envisage on formal methods for cloud computing (2013-2016). Einar Broch Johnsen is the deputy director of the Sirius Centre for research driven innovation on scalable data access.