Published: 25th October 2016
DOI: 10.4204/EPTCS.228
ISSN: 2075-2180

EPTCS 228

Proceedings of the First International Workshop on
Formal Methods for and on the Cloud
Reykjavik, Iceland, 4th June 2016

Edited by: Razieh Behjati and Ahmed Elmokashfi

Preface
Actors and Meta-Actors: Two-Level for Reasoning about Cloud Infrastructure
Gul Agha
1
Static Analysis Using the Cloud
Rahul Kumar, Chetan Bansal and Jakob Lichtenberg
2
Modeling Deployment Decisions for Elastic Services with ABS
Einar Broch Johnsen, Ka I Pun and S. Lizeth Tapia Tarifa
16
Configuring Cloud-Service Interfaces Using Flow Inheritance
Pavel Zaichenkov, Olga Tveretina and Alex Shafarenko
27
An Enhanced Model for Stochastic Coordination
Nuno Oliveira and Luis Soares Barbosa
35

Preface

This volume contains the proceedings of iFMCloud 2016, the First International Workshop on Formal Methods for and on the Cloud, which was held on June 4, 2016 in Reykjavik, Iceland as a satellite event of the 12th International Conference on integrated Formal Methods (iFM 2016).

Cloud solutions are increasingly used for a plethora of purposes, including solving memory-intensive and computation-intensive problems. Ensuring the reliability, availability, scalability, and security of cloud solutions, as networked distributed systems with properties such as dynamic reallocation of resources, is a challenging problem that requires rigorous modeling, analysis, and verification tools. Such tools can be devised using the techniques provided by the formal methods community. On the other hand, many formal analysis and verification tools are memory-intensive and computation-intensive, which can benefit from the cloud technology.

The goal of the iFMCloud workshop is to identify and better understand challenges of using formal and semi-formal methods for modeling and verification of Cloud-based systems and computer and communication networks, as well as challenges and opportunities in providing formal analysis and verification as services on the Cloud.

The iFMCloud 2016 program consisted of a keynote talk by Gul Agha, four invited and contributed papers, and two working sessions. During the workshop, we heard about the configuration of cloud-service interfaces using flow inheritance; an extension of Stochastic Roe, which is more scalable and therefore allows specifying and analyzing cloud applications; the use of ABS simulations for making decisions about the deployment of services on the cloud; and finally accelerated execution of large test-suites through parallel invocation of SVD (static device driver) using Microsoft Azure.

We would like to thank our keynote speaker and the authors of invited and contributed papers. We also would like to thank the program committee who provided thorough evaluation of the contributions and insightful comments and suggestions for the authors. We are grateful to the iFM organization committee for the logistical support of the workshop.

Program Chairs

Razieh Behjati, Simula Research Laboratory, Norway
Ahmed Elmokashfi, Simula Research Laboratory, Norway

Program Committee

Eva Darulova, MPI-SWS, Germany
Fatemeh Ghassemi, University of Tehran, Iran
Arnaud Gotlieb, Simula Research Laboratory, Norway
Ernst Gunnar Gran, Simula Research Laboratory, Norway
Hossein Hojjat, Cornell University, USA
Geir Horn, University of Oslo, Norway
Andreas Kassler, Karlstad University, Sweden
Steven Latre, University of Antwerp - iMinds, Belgium
Meriem Ouederni, IRIT/INPT Toulouse, France
Rosario Pugliese, University of Florence, Italy
Sven-Arne Reinemo, Fabriscale Technologies, Norway
Hamideh Sabouri, Shahid Beheshti University, Iran
Jesus Escudero Sahuquillo, Technical University of Valencia, Spain
Sagar Sen, Simula Research Laboratory, Norway
Marjan Sirjani, Reykjavik University, Iceland
Martin Steffen, University of Oslo, Norway
Amirhossein Taherkordi, University of Oslo, Norway

Actors and Meta-Actors: Two-Level for Reasoning about Cloud Infrastructure

Gul Agha (University of Illinois at Urbana-Champaign)

Cloud Computing involves a very large numbers of actors. Actors have to work together to achieve the system goals; coordination protocols describe the interaction patterns to achieve such goals. We will discuss the problem of efficiently implementing large-scale computing on the clouds while achieving security and coordination between large numbers of actors. Coordination protocols impose constraints on the message flow--thus enforcing specific multi-party session types. However, coordination protocols may also provide a vector for Denial of Service attacks as well as for Information Leakage. Moreover, adaptation in cloud computing requires metaprogramming and computational reflection. Reasoning about protocols for coordination separately from the application level actor code can be facilitated by a two-level actor semantics. The talk will describe mechanisms for coordination and methods for formally reasoning about them.