|
Published: 25th October 2016 DOI: 10.4204/EPTCS.228 ISSN: 2075-2180 |
| 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 |
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.
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.