Coordination Models and Languages: 24th IFIP WG 6.1 International Conference, COORDINATION 2022 Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022 Lucca, Italy, June 13–17, 2022 Proceedings

Foreword
Preface
Organization
Contents
Invited Presentation
Formal Methods for Socio-technical Security
	1 Introduction
	2 From Technical to Socio-technical Security
	3 Formal and Automated Analysis of Security Ceremonies
	References
Timed and Probabilistic Systems
MIMOS: A Deterministic Model for the Design and Update of Real-Time Systems
	1 Motivation
	2 Contributions and Related Work
	3 The MimosModel
		3.1 Preliminaries on KPN
		3.2 Timed Kahn Process Networks
		3.3 Mimos: TKPN with Registers
		3.4 Design and Update with Mimos
	4 Fixed-Point Semantics
		4.1 Preliminaries on KPN ch2kahn1974
		4.2 Semantics of Timed KPN
		4.3 Adding Registers to Timed KPN
	5 Analysis Problems
	6 Conclusions
	References
A Sound Up-to-n, Bisimilarity for PCTL
	1 Introduction
	2 PCTL
	3 Up-to-n, Bisimilarity
	4 Soundness
	5 Conclusions
	References
Collective Adaptive Systems and Aggregate Computing
Extensible 3D Simulation of Aggregated Systems with FCPP
	1 Introduction
	2 Background
		2.1 Collective Adaptive Systems
		2.2 Aggregate Programming
		2.3 FCPP
		2.4 OpenGL
	3 Extending FCPP with a Graphical User Interface
		3.1 Features
		3.2 Architecture
		3.3 Technical Challenges
		3.4 Comparison with Protelis and Scafi
	4 Case Studies
		4.1 Composition of Spreading and Collection Blocks
		4.2 Broadcast Through a Self-organising Channel
		4.3 Peer-to-peer Message Dispatch
		4.4 Random Walk in an Apartment
	5 Conclusion
	References
Towards Reinforcement Learning-based Aggregate Computing
	1 Introduction
	2 Background
		2.1 Aggregate Computing
		2.2 The Gradient Building Block
		2.3 Reinforcement Learning
	3 Reinforcement Learning-based Aggregate Computing
		3.1 On Integrating Machine Learning and Aggregate Computing
		3.2 Aggregate Programs Improvement Through RL
		3.3 Building Blocks Refinement
		3.4 Reinforcement Learning-based Gradient Block
	4 Evaluation
		4.1 Simulation Setup
		4.2 Results and Discussion
	5 Conclusion
	References
Sibilla: A Tool for Reasoning about Collective Systems
	1 Sibilla in a Nutshell
		1.1 Sibilla Back End
		1.2 Sibilla Specification languages
		1.3 Sibilla front ends
	2 Sibilla at Work
	3 Concluding Remarks
	References
Space-Fluid Adaptive Sampling: A Field-Based, Self-organising Approach
	1 Introduction
	2 Motivation and Related Work
	3 Distributed Aggregate Sampling: Model
		3.1 Computational Model
		3.2 Self-stabilisation
		3.3 Problem Definition
	4 Aggregate Computing-Based Solution
	5 Evaluation
		5.1 Scenario
		5.2 Parameters
		5.3 Metrics
		5.4 Implementation and Reproducibility
		5.5 Results
	6 Conclusions and Future Work
	References
Processes and Languages
Formal Choreographic Languages
	1 Introduction
	2 Formal Choreographic Languages
	3 Correctness and Completeness
	4 Communication Properties
	5 Communication Properties by Construction
	6 Global Types as Choreographic Languages
	7 Choreography Automata
	8 Concluding Remarks
	References
A Model of Actors and Grey Failures
	1 Introduction
	2 Informal Overview
	3 A Model of Failures
	4 Calculus for Cursed Systems
		4.1 Basic Properties of Systems Reductions
	5 Properties of Cursed Systems
		5.1 Resilience and Recoverability
		5.2 Augmentation of Cursed Systems
		5.3 Augmentation with Scoped Barbs
	6 Conclusion and Related Work
	References
Soft Concurrent Constraint Programming with Local Variables
	1 Introduction
	2 An Introduction to Residuated Monoids
		2.1 Preliminaries on Ordered Monoids
		2.2 Remarks on Residuation
	3 A Polyadic Approach to Constraint Manipulation
		3.1 Cylindric and Polyadic Operators for Ordered Monoids
		3.2 Cylindric and Polyadic Operators for Residuated Monoids
		3.3 Polyadic Soft Constraints
	4 Polyadic Soft CCP: Syntax and Reduction Semantics
		4.1 Reduction Semantics
		4.2 Saturated Bisimulation
	5 Labelled Reduction Semantics
	6 Semantics Correspondence and Labelled Bisimilarity
		6.1 On the Correspondence Between Reduction Semantics
		6.2 Labelled Bisimulation
	7 Related Works
	8 Conclusions and Further Works
	References
Runtime Verification and Monitor Synthesis
A Synthesis Tool for Optimal Monitors in a Branching-Time Setting
	1 Introduction
	2 Preliminaries
		2.1 The Specification Logic
		2.2 Monitorability in RecHML
		2.3 Extending the Limits of Monitorability
	3 Design and Implementation
		3.1 Disjunctive Form
		3.2 Step 1: Eliminating Existential Modalities
		3.3 Step 2: Eliminating Least Fixed Points
		3.4 Step 3: Eliminating Disjunctions
	4 The Tool
		4.1 Internal Architecture
		4.2 Usage
	5 Evaluation
	6 Conclusion
		6.1 Future Work
		6.2 Related Work
	References
A Monitoring Tool for Linear-Time HML
	1 Introduction
	2 The Logic
		2.1 Trace Properties
	3 Monitor Synthesis
	4 Implementation
		4.1 Refining the Model
		4.2 The Monitor Synthesis
		4.3 The Monitoring Algorithm
		4.4 Monitor Instrumentation
	5 Case Study
	6 Conclusion
	References
Microservices
Model-Driven Generation of Microservice Interfaces: From LEMMA Domain Models to Jolie APIs
	1 Introduction
	2 Encoding LEMMA Domain Modelling Concepts in Jolie
		2.1 LEMMA Domain Modelling Concepts
		2.2 Jolie Types and Interfaces
		2.3 Encoding LEMMA Domain Models as Jolie APIs
		2.4 Applying the Encoding
	3 LEMMA2Jolie: A Code Generator to Derive Jolie APIs from LEMMA Domain Models
	4 Related and Future Work
	References
Author Index