Programming languages based on the actor model such as Erlang and Elixir rely on message passing for communication. A core concept of this communication model are mailboxes: all actors are allowed to send messages to a mailbox, but only its owner may retrieve them. A major challenge in such systems is detecting and eliminating protocol violations and deadlocks. Mailbox types are a novel type system that enables static reasoning about the contents of mailboxes, but the metatheory of mailbox type systems is complex and requires extensive reasoning about subtyping. This paper establishes a machine-checked foundation for mailbox types. As a basis for this, we formalize Pat, the first programming language to use mailbox types, in Rocq. With its help, we identified and corrected several oversights in the original definitions. Furthermore, we provide mechanized proofs of several properties of the semantics of mailbox types and the substitution lemma for Pat.
Guaranteeing cyber-physical systems (CPSs) correct and proper behaviour is an essential and challenging issue, as they are widely used in many application domains. This paper aims to contribute to the flexible design and development of structured CPSs, composed of similar elements and capable of (self-)adaptation to satisfy evolving internal and external constraints, e.g. using control theory. To this end, based on a model of a hierarchical motif for modeling both systems’ elements and controllers, we introduce a control-compatible notion of a motif refinement, and then we show that the stability of control can be preserved regarding a refinement-based development. Motivations and contributions are illustrated by the smart building example.
We enable deductive verification for Stipula, a domain-specific language for legal contracts, by systematically translating contracts into Java programs annotated with Java Modeling Language specifications, and subsequently proving them using a deductive verification tool. A central challenge of the translation lies in representing event-driven and time-dependent behaviour within a static specification framework. To address this, we introduce a dispatch table that records schedulable events together with their triggering times. The technique is presented for acyclic Stipula contracts. We also extend the proposed technique to cyclic contracts, outlining the additional challenges and the conditions under which the approach remains applicable.
In large-scale distributed systems, such as the Internet of Things (IoT), min-max consensus algorithms provide a mechanism for collective coordination by enabling nodes to converge on a “best” value produced by one of the participants in the computation. However, min-max consensus algorithms are monotonic and non-self-stabilizing by nature: once a value is merged into the aggregate it cannot be retracted, leading to propagation of stale or incorrect data in the presence of transient faults or topology changes. In this work, we propose a novel self-stabilizing min-max consensus algorithm ensuring convergence to the best available value in the network by propagating information along shortest valid paths. Each gossip message carries a value and path of nodes that have acknowledged it, enabling loop-freedom and natural pruning of obsolete contributions. We rely on field-based coordination and specifically the Aggregate Computing paradigm to present the algorithm, prove self-stabilization, and provide an implementation as a reusable library for the Collektive DSL. This work contributes a foundational building block for resilient coordination in pervasive computing systems, paving the way to more complex, self-stabilizing distributed applications.
The verification and validation of collective adaptive systems is a challenging task, typically tackled through a combination of approaches including formal analysis, simulation, Hardware-in-the-Loop, and real-world experimentation. One critical aspect of simulation concerns the trade-off between realism and scalability. A typical validation pipeline involves initial simulation of large-scale scenarios with simplified models of the world, and detail is gradually increased in subsequent steps, introducing more realistic physical and environmental dynamics. An underexplored opportunity in this context lies in leveraging game development platforms to achieve high-fidelity simulations. In this work, we explore the integration of an existing implementation of aggregate programming, a common paradigm for engineering collective adaptive systems, with Unity, a widely used game development platform. We show that this integration is feasible even though the two systems were not designed to work together, we discuss the technical challenges that were encountered and the limitations of the approach, while highlighting the potential for such integration to enhance simulation realism in the study of collective adaptive systems.
We introduce expressions formed from distributed timed scenarios. Such expressions allow us to specify complex distributed behaviours in a hierarchical fashion. We define the semantics and consistency of a scenario expression. We then address the problem of realisability of sets of sequential timed scenarios as scenario expressions and present an efficient algorithm which produces a non-trivial scenario expression that preserves the semantics of the original set of scenarios. Our method directly handles explicit time constraints and produces a scenario expression whose time constraints are inferred from those of the realised set.
Accurate indoor localisation is a key enabling technology for many distributed systems, including collective robotics, smart environments, and user wearable devices. In these settings, localisation must often be achieved without central coordination, under limited sensing capabilities, and in the presence of dynamic environmental changes. Collective indoor localisation algorithms address these challenges by exploiting local interactions among devices to collectively infer positions. However, many existing approaches implicitly assume relatively stable conditions and offer limited guarantees on adaptability and resilience. In this paper, we investigate cooperative indoor localisation from a self-adaptive perspective. We reformulate two established localisation algorithms within the aggregate programming framework, and propose novel variants of them to improve their performance. We evaluate our proposals through extensive simulation, analysing error and communication cost across a wide range of scenarios, including recovery from disruptive events. Our results uncover the trade-offs between accuracy, resiliency and efficiency, shedding light on the design space of what we call aggregate indoor localisation algorithms.
Multiparty languages provide a concrete foundation for expressing complex coordination behaviors in a single, coherent specification. Based on this idea, several paradigms have been proposed in the literature over the years. Among them, choreographic programming is a widely adopted paradigm for defining deadlock-free distributed systems, while multitier programming takes a different approach, focusing on partitioning system logic across different execution tiers. Recognizing that these paradigms share fundamental similarities as multiparty languages, we build on choreographic programming while importing static architectural descriptions and placement types inspired by ScalaLoci. We introduce ScalaTropy, a coordination language that integrates multiple communication schemes to establish both isotropic and anisotropic communication patterns, while incorporating placement types and type-level architecture specification inspired by ScalaLoci, advancing beyond the capabilities of traditional choreographic languages. We provide a Scala implementation leveraging monadic constructs, which cleanly separate the language specification from the underlying monadic effects that drive coordination mechanisms. Finally, we present an empirical evaluation demonstrating the language’s expressiveness and an analysis of communication overhead.
Although it is ubiquitous, machine learning still faces two major challenges: explainability and privacy. To address the first challenge, this paper focuses on Inductive Logic Programming (ILP), a framework for learning declarative, symbolic, and interpretable models from multi-relational data. However, existing ILP systems are fundamentally centralized, an assumption that conflicts with privacy requirements and with many real-world scenarios in which data are inherently distributed and cannot be shared. To overcome this limitation and address the second challenge, we introduce Bach4Popper, a federated ILP framework that combines Popper, an ILP learning system, with Bach, a coordination language developed by the authors. We show, both theoretically and empirically, that Bach4Popper is correct with respect to the corresponding centralized version of Popper. Experimental results further demonstrate that computational performance is preserved when moving from a centralized to a federated setting.
We propose a programming pattern for runtime architectural adaptation of service-oriented applications. Our approach enables transparent reconfiguration of distributed services at runtime leveraging on the key features for dynamic discovery binding of services supported developed in an existing platform. More precisely, in this paper we equip the platform with monitoring capabilities supporting the transparent reconfiguration of the architecture of service-oriented applications triggered by changes in the execution context. We demonstrate the effectiveness of the approach on the adaptable TeaStore benchmark.
Collective Adaptive Systems (CAS) are groups of heterogeneous components that interact to achieve local and global goals. One way to view CAS is to consider them as intelligent agents that operate according to a behaviour based on observations and a state. Internet-of-Things (IoT) ecosystems provide a natural application domain for agent-based solutions to support modelling and analysis, as they share many architectural similarities. In this paper, we show how one of the recently proposed agenda-based languages, named YODA, can be used to support the design and engineering of an IoT system designed to measure indoor air quality and warn if it falls below a given threshold. The proposed model has been simulated using the tool Sibilla to forecast how battery life, coverage, and overall Indoor Air Quality evolve with the number of people in a building. In the paper, we show how the proposed methodology can be used during the design phase to support developers and engineers and aid their decision-making, without relying on real-world deployment.
Reasoning about consistency models for replicated data systems is a challenging task that requires a deep understanding of both the consistency models themselves and a large part of human inputs in mechanized verification approaches. In this work, we introduce an approach to reasoning about consistency models for replicated data systems. We introduce HistMSO, a monadic second-order logic (MSO) for histories and abstract executions, the formal models of executions of replicated data systems introduced by Burckhardt. We show that HistMSO can express 39 out of 42 consistency models from Viotti and Vukolic hierarchy. Moreover, we develop a method for reducing HistMSO satisfiability and model-checking to the same problems for MSO over words. While doing this, we leverage the MONA tool for automated reasoning on consistency models.
Aggregate programming is a field-based coordination paradigm with over a decade of exploration and successful applications across domains including sensor networks, robotics, and IoT, with implementations in various programming languages, such as Protelis, ScaFi (Scala), and FCPP (C++). A recent research direction integrates machine learning with aggregate computing, aiming to support large-scale distributed learning and provide new abstractions for implementing learning algorithms. However, existing implementations do not target data science practitioners, who predominantly work in Python—the de facto language for data science and machine learning, with a rich and mature ecosystem. Python also offers advantages for other use cases, such as education and robotics (e.g., via ROS). To address this gap, we present Phyelds, a Python library for aggregate programming. Phyelds offers a fully featured yet lightweight implementation of the field calculus model of computation, featuring a Pythonic API and an architecture designed for seamless integration with Python’s machine learning ecosystem. We describe the design and implementation of Phyelds and illustrate its versatility across domains, from well-known aggregate computing patterns to federated learning coordination and integration with a widely used multi-agent reinforcement learning simulator.
We describe , a user-friendly web-based front-end tool for the Rebeca language, based on the Caos library for Scala. can simulate different operational semantics of (timed) Rebeca, thus facilitating the dissemination and awareness of Rebeca, providing insights into the differences among existing semantics for Rebeca, and supporting quick experimentation of new Rebeca variants (e.g., when the order of received messages is preserved). The tool also comes with initial reachability analyses for Rebeca models (e.g., the possibility of reaching deadlocks or desirable states). We illustrate the tool by means of a ticket service use case from the timed Rebeca literature.
We propose a mechanism for selecting distributed services which encompasses three orthogonal, yet related type of contracts’ compliance. Indeed, we envisage contract compliance as the intersection of behavioural contract compliance with the compliance of functional and non-functional contracts. We model services as communicating-finite state machines (CFSMs) suitably extended to capture data-awareness and application-level quality-of-service (QoS). This extension is instrumental to define our notion of contract compliance in terms of a bisimulation relation for this new class of CFSMs. More precisely, we introduce CFSMs where transitions are decorated with constraints on the payloads while states of CFSMs have decorations that carry QoS contracts. This allows us to capture behavioural contracts (considering the communication pattern as usual in systems of CFSMs) as well as functional and non-functional contracts. We use a case study to assess our approach and we discuss tool support for our framework.
The Reowolf project developed connectors as a replacement of two-party network sockets for multi-party communication in next-generation internet applications. Users control connectors via protocols in the bespoke protocol description language (PDL), which is based on synchronous languages such as Reo and Esterel. The novelty lies in the emphasis on dynamism: users refine protocols throughout their execution. We formalise the semantics of PDL, distinguishing dual notions of protocol behaviour: accepted behaviour is highly (de)compositional and specifies what communication is allowed, while constructed behaviour arises from protocol execution and accounts for how execution steps interdepend and interleave via messages sent and received. Toward machine-checking the correctness of the connector runtime reference implementation, we specify the API and correctness criteria of PDL runtime systems.
Concurrent and distributed systems are often prone to failures. Errors in modeling an agent's behavior can propagate into large interacting systems with unexpected consequences. In this paper, we propose a theory for the process algebra CCS enriched with a formal and explicit representation of errors based on McCarthy's style three-valued logic, which includes the traditional Boolean values and a third error value. In this setting, we formally study how the emergence of local errors may or may not result in propagation, as also emphasized in a real-world case study modeling a distributed microservices architecture.
Messaging protocols for resource limited systems such as distributed IoT systems are often vulnerable to attacks due to security choices made to conserve resources such as time, memory, or bandwidth. Protocol dialects are a light weight, modular mechanism to provide security guarantees such as authentication or integrity. In this paper we propose a generic dialect for the Constrained Application Protocol (CoAP) messaging protocol. The CoAP protocol, dialect, and an attack models are formalized in the rewriting logic system Maude. A number of properties relating CoAP and its dialected form are given, including a stuttering bisimulation, thus ensuring that dialecting preserves important properties of a CoAP application. The ideas are illustrated with some simple scenarios.
Choreographies are useful for modelling systems with multiple simultaneously executing and communicating participants, e.g. distributed systems. VeyMont can verify correctness of choreographies and generate verifiably correct code that implements the choreography. Initially, it supported only fixed sets of participants. However, realistic systems are often parameterized: they scale according to some parameter N. This paper extends VeyMont with parameterized choreographies, making VeyMont more usable for realistic case studies. Specifically, we add parameterized primitives such as participant families and parameterized communication. We encode these primitives using a structured parallelism primitive from the underlying verifier VerCors, and by using conditionals in the endpoint projection, partially delaying projection until run time. We illustrate the encoding with a distributed summation choreography, and prove it correct with VerCors.
Aggregate computing is a paradigm with over a decade of investigation and multiple programming frameworks available, which proved to be particularly suitable for the simulation of applications in challenging domains such as smart cities and robot swarms. This paper introduces a toolchain for practical multi-robot demonstrations based on aggregate computing principles, and validates it with a live interactive demo in an open-public event in the context of the European Researchers' Night. More specifically, we show how we coordinated a team of mobile robots to form spatial patterns. We discuss the practical demonstration performed in an indoor environment, which exploits a camera system and ArUco markers for localization.
