This book constitutes the refereed proceedings of the 25th IFIP WG 6.1 International Conference on Coordination Models and Language, COORDINATION 2023, held in Lisbon, Portugal, in June 2023, as part of the 18th International Federated Conference on Distributed Computing Techniques, DisCoTec 2023. The 12 regular papers and 2 short paper presented in this book were carefully reviewed and selected from 27 submissions. The papers deal with the following topics: Collective Adaptive Systems and Aggregate Computing; Cyber-Physical Systems; Verification and Testing; Languages and Processes; and Run-Time Changes. Foreword Preface Organization Contents Keynote Relating Message Passing and Shared Memory, Proof-Theoretically 1 Introduction 2 Proof Reduction as Communication 3 Asynchronous Communication 4 A Language for Asynchronous Communication 4.1 The Dynamics of Process Configurations 4.2 Positive Connectives 4.3 Refactoring the Rules of Computation 4.4 Process Definitions 4.5 Some Examples 4.6 Negative Connectives 4.7 Identity as Forwarding 5 Preservation and Progress 6 Linear Futures 6.1 Statics and Dynamics of Futures 6.2 Shared Memory Examples 7 From Linear to Nonlinear Futures 8 Backporting Persistence to Message Passing 8.1 Examples 8.2 Metatheory 9 Conclusion References Collective Adaptive Systems and Aggregate Computing MacroSwarm: A Field-Based Compositional Framework for Swarm Programming 1 Introduction 2 Context and Motivation 3 Background: Aggregate Computing 4 MacroSwarm 5 Evaluation 5.1 Case Study: Find and Rescue 5.2 Discussion 6 Related Work 7 Conclusion and Future Work References ScaRLib: A Framework for Cooperative Many Agent Deep Reinforcement Learning in Scala 1 Introduction 2 Background 2.1 Reinforcement Learning 2.2 Multi Agent Reinforcement Learning 2.3 Alchemist 2.4 ScaFi 3 ScaRLib 3.1 Core Abstraction 3.2 ScaFi-Alchemist Integration: 3.3 DSL for Learning Configurations 3.4 Tool Usage 4 Experiments 4.1 Scenario Description 4.2 Results 5 Related Work 6 Conclusion and Future Work References Programming Distributed Collective Processes for Dynamic Ensembles and Collective Tasks 1 Introduction 2 Context, Related Work, and Motivation 3 Background: The eXchange Calculus 3.1 System Model 3.2 XC Key Data Type: Neighbouring Values 4 Distributed Collective Processes in XC 4.1 Modelling on Event Structures 4.2 Formalisation 5 Discussion and Proof-of-Concept 5.1 The DCP Abstraction 5.2 Features of the Abstraction and Programming Model 5.3 Examples 5.4 Proof-of-Concept Implementation 6 Conclusion References Cyber-Physical Systems Shelley: A Framework for Model Checking Call Ordering on Hierarchical Systems*-12pt 1 Introduction 2 Overview 2.1 Restricting the Behavior and Usage of Systems 2.2 Encapsulation Complicates Verification 3 The Shelley Language 4 The Shelley Framework 4.1 System Declaration 4.2 Behavior Generation 4.3 Valid Behavior Checking 4.4 Model Generation and Claim Checking 5 Evaluation 5.1 Verifying Aquamote® with Shelley 5.2 Performance Impact of Behavior Checking 6 Related Work 7 Conclusion References Stark: A Software Tool for the Analysis of Robustness in the unKnown Environment 1 Introduction 2 The Model 2.1 Case Study: Unmanned Ground Vehicles 3 The Robustness Temporal Logic 4 The Stark Tool 5 The Tool in Action 6 Concluding Remarks References Verification and Testing RSC to the ReSCu: Automated Verification of Systems of Communicating Automata 1 Introduction 2 Communicating Automata 3 ReSCu 4 Results 5 Conclusion References .28em plus .1em minus .1emReasoning About Choreographic Programs 1 Introduction 2 Language 2.1 Syntax 2.2 Semantics 3 A Hoare Calculus for Choreographies 3.1 State Logic 3.2 Hoare Logic 4 Completeness of the Hoare Calculus 4.1 Weakest Liberal Preconditions 4.2 Completeness 4.3 Decidability 5 Related Work 6 Conclusions References Caos: A Reusable Scala Web Animator of Operational Semantics*-12pt 1 Introduction 2 Use-Case: A While-Language for Teaching 3 Use-Case: Analysing Choreographies in Research 4 Caos framework 5 Conclusions and Lessons Learned References JoT: A Jolie Framework for Testing Microservices 1 Introduction 2 Methodology and Structure of Tests 2.1 Building a Test in JoT 2.2 Writing a Complete Test 2.3 Executing JoT Tests 3 Validation 3.1 Tested Interaction Scenarios 3.2 JoT Test of Scenario 1 3.3 JoT Test of Scenario 2 4 Related Work, Discussion, and Conclusion References Languages and Processes Rollback Recovery in Session-Based Programming 1 Introduction 2 A Reversible Video on Demand Service Example 3 The cherry-pi Calculus 4 Rollback Safety 5 Properties of cherry-pi 6 Conclusion and Related Work References Safe Asynchronous Mixed-Choice for Timed Interactions 1 Introduction 2 Timeout Asynchronous Session Types (TOAST) 2.1 Syntax of TOAST 2.2 Semantics of TOAST 2.3 Duality, Well-formedness, and Progress 3 A Calculus for Processes with Timeouts 3.1 Process Reduction 4 Expressiveness 4.1 Missing Deadlines 4.2 Ping-Pong Protocol 4.3 Mixed-Choice Ping-Pong Protocol 4.4 Message Throttling 5 Concluding Discussion References A Formal MDE Framework for Inter-DSL Collaboration 1 Introduction 2 Case Study and Motivation 2.1 Configuration Management DSL (CM-DSL) 2.2 Security Risk Assessment DSL (SRA-DSL) 2.3 Collaboration and Verification Needs 3 Inter-DSL Collaboration: A Model-based Architecture 3.1 Formal Model Driven DSLs 3.2 Formal Model Driven Inter-DSL Collaboration 4 Application to Smart Grid System 4.1 Modeling DSLs and Their Collaboration 4.2 Formalization of Metamodels 4.3 BPMN Formalization with a CSP Transformation 4.4 Discussion 5 Related Work 6 Conclusion References Run-Time Changes Legal Contracts Amending with Stipula 1 Introduction 2 From Stipula to higher-order Stipula 3 Examples of Amendments 4 Semantics 5 Constraining Amendments 6 Agreement on Amendments 7 Related Works 8 Conclusions References Toward Run-time Coordination of Reconfiguration Requests in Cloud Computing Systems 1 Introduction 2 Motivating Example 3 Background 3.1 Feature Models 3.2 JavaBIP Component-Based Approach 4 Design and Transformation 4.1 From Features to Components 4.2 Component Behaviour Generation 4.3 Coordination Layer Generation 5 CBVM to Deal with Reconfigurations 6 FeCo4Reco Implementation and Experiments 7 Related Work 8 Conclusion and Future Work References Author Index
