Published: 7th July 2016
DOI: 10.4204/EPTCS.217
ISSN: 2075-2180


Proceedings of the Workshop on
FORmal methods for the quantitative Evaluation of Collective Adaptive SysTems
Vienna, Austria, 8 July 2016

Edited by: Maurice H. ter Beek and Michele Loreti

Maurice H. ter Beek and Michele Loreti
Invited Presentation: Modeling and simulation of collective adaptive systems: a case for self-adaptive software and domain-specific languages
Adelinde M. Uhrmacher
Invited Presentation: Probabilistic Programming, Estimation, and Euclidean Model Checking for Aggregate Behavior of Concurrent Systems
Gul A. Agha
Invited Presentation: Resiliency with Aggregate Computing: State of the Art and Roadmap
Mirko Viroli and Jacob Beal
A Formal Framework for Modeling Trust and Reputation in Collective Adaptive Systems
Alessandro Aldini
Data as processes: introducing measurement data into CARMA models
Stephen Gilmore
Modelling movement for collective adaptive systems with CARMA
Natalia Zoń, Vashti Galpin and Stephen Gilmore
On Formal Methods for Collective Adaptive System Engineering. Scalable Approximated, Spatial Analysis Techniques. Extended Abstract.
Diego Latella
Challenges in Quantitative Abstractions for Collective Adaptive Systems
Mirco Tribastone
Stochastic and Spatial Equivalences for PALOMA
Paul Piho and Jane Hillston
From Collective Adaptive Systems to Human Centric Computation and Back: Spatial Model Checking for Medical Imaging
Gina Belmonte, Vincenzo Ciancia, Diego Latella and Mieke Massink


These proceedings contain the papers that were presented at the Workshop on FORmal methods for the quantitative Evaluation of Collective Adaptive SysTems (FORECAST), which took place on 8 July 2016 in Vienna, Austria, as a satellite event of the 4th federated event on Software Technologies: Applications and Foundations (STAF 2016).

FORECAST's primary goal is to raise awareness in the software engineering and formal methods communities of the particularities of Collective Adaptive Systems (CAS) and the design and control problems which they bring. Therefore, the workshop is sponsored by the FP7-ICT-600708 European project QUANTICOL (A Quantitative Approach to Management and Design of Collective and Adaptive Behaviours), that runs from 2013-2017.

CAS consist of a large number of spatially distributed heterogeneous entities with decentralised control and varying degrees of complex autonomous behaviour that may be competing for shared resources even when collaborating to reach common goals. It is important to carry out thorough quantitative modelling and analysis and verification of their design to investigate all aspects of their behaviour before they are put into operation. This requires combinations of formal methods (e.g. stochastic process algebras and associated verification techniques, like quantitative model checking) and applied mathematics (e.g. mean field/continuous approximation and control theory) which moreover scale to large-scale CAS.

ICT-based CAS are at the core of the envisioned smart cities of the future, which are on the research agenda of many EU and other international institutions and think-tanks. In fact, case studies in the QUANTICOL project concern smart urban transport (e.g. bike-sharing systems) and smart grids, i.e. systems of heterogeneous components with competing goals that must manage resources in a fair and efficient way. This is particularly challenging when designing for behaviour that is emergent and spatially inhomogeneous, but must nevertheless be guaranteed to satisfy operational requirements.

As a satellite event of STAF 2016, FORECAST is co-located with the 14th International Conference on Software Engineering and Formal Methods (SEFM 2016), thus providing an excellent opportunity for exchanging results and experiences on applying quantitative modelling and analysis techniques from formal methods and software engineering and technologies.

The workshop received five regular paper submissions and we invited two active researchers from the QUANTICOL project, Diego Latella (ISTI-CNR, Italy) and Mirco Tribastone (IMT Lucca, Italy), to submit extended abstracts of invited talks on their latest results from the project presented into a broader context. No less than four Program Committee members reviewed these submissions. Furthermore, the workshop included three keynote talks by renowned experts on the workshop topics, on the crossroads of SEFM and QUANTICOL, not participating in the project: Adelinde Uhrmacher (University of Rostock, Germany), Gul Agha (University of Illinois at Urbana-Champaign, USA), and Mirko Viroli (University of Bologna, Italy). We hereby thank all these invited speakers for accepting our invitation.

Thanks are also due to the Program Committee members, listed below, for their careful and swift reviewing. We are grateful to the STAF Workshop Chairs, Manuel Wimmer (TU Wien, Austria), Dániel Varró (Budapest University of Technology and Economics, Hungary), and Paolo Milazzo (University of Pisa, Italy), for accepting FORECAST as a satellite event at STAF 2016 and to the STAF organisers, General Chair Gerti Kappel (TU Wien, Austria) and Organization Chair Tanja Mayerhofer (TU Wien, Austria) for the smooth organisation and the pleasant interaction concerning organisational matters. We would also like to take this opportunity to thank Andrei Voronkov for his excellent EasyChair system that automates most of the tasks involved in organising and chairing a workshop. Finally, we thank EPTCS and its editor-in-chief, Rob van Glabbeek, for agreeing to publish the proceedings of FORECAST 2016.

Program Chairs

Program Committee

Modeling and simulation of collective adaptive systems: a case for self-adaptive software and domain-specific languages

Adelinde M. Uhrmacher (University of Rostock, Germany)

Collective adaptive systems we interpret as systems that operate on different organizational levels and whose structures, in terms of components and interactions, are changing over time. These systems provide specific challenges for modeling as well as simulation methods. First, modeling languages have to be sufficiently expressive to be able to capture the essentials of collective adaptive systems. We present the multi-level modeling languages ML-Rules, ML-Space, and ML3, and discuss their features that facilitate developing and maintaining compact models of collective adaptive systems. Second, experimentation languages like SESSL can facilitate specifying, executing, and documenting complex "in-silico" experiments, e.g., parameter scans, statistical model checking, or optimization experiments comprising multiple executions and analysis steps.

However, executing experiments with complex models comes at a price. E.g., in the case of ML-Rules, allowing arbitrary functions not only on attributes and content but also for specifying reaction kinetics on the fly prevents us from taking short cuts that simulators for less expressive languages can take. A family of execution algorithms, from which a suitable algorithm can be selected and configured on demand before or during simulation, helps an efficient execution. Intelligent strategies for automatically selecting and configuring algorithms do not only come handy for executing models, but also for identifying and configuring suitable methods for the diverse analysis steps involved in simulation experiments. A pre-requisite for this kind of self-adaptation is a clear separation of concern and a component-based software design, as realized in the modeling and simulation framework James II.

Thus, similarly as domain-specific languages support users in developing and maintaining models of collective adaptive system, and specifying, executing, and documenting experiments, flexible, self-adaptive simulation environments contribute to more efficient and effective experimenting with these models.

Probabilistic Programming, Estimation, and Euclidean Model Checking for Aggregate Behavior of Concurrent Systems

Gul A. Agha (University of Illinois at Urbana-Champaign, USA)

In many real-world applications, such as those involving biological systems or big data, only probabilistic "guarantees" of approximate behavior are feasible. Moreover, we are often interested in aggregate behavior of such systems. The talk will describe probabilistic programming and methods for estimation which can guide the execution of probabilistic programs. Such methods are based on sampling the behavior of a concurrent system and closely connected to statistical model checking. I will then present Euclidean model checking, a method for analyzing quantitative properties of systems. The approach will be illustrated with applications such as Pharmacokinetics and sensor networks.