This book constitutes the refereed proceedings of the 24th IFIP WG 6.1 International Conference on Coordination Models and Language, COORDINATION 2022, held in Lucca, Italy, in June 2022, as part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022. The 11 regular papers and one short paper presented in this book were carefully reviewed and selected from 22 submissions. COORDINATION provides a well-established forum for the growing community of researchers interested in coordination models and languages, architectures, verification and implementation techniques necessary to cope with the complexity induced by the demands of today's software development. 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
