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