Abstract Distributed runtime verification (DRV) addresses the problem of checking the correctness of distributed systems during execution, coping with partial knowledge, dynamic topologies, and the absence of global time. These challenges are particularly prominent in proximity-based networks, such as those arising in IoT and Far Edge computing scenarios, where large numbers of devices interact through local communication. This tutorial presents an approach to DRV based on Aggregate Programming (AP), a paradigm for designing distributed collective systems via high-level abstractions over computational fields. We show how temporal and spatial properties (expressed in past-CTL and SLCS, respectively) can be systematically compiled into aggregate monitors grounded in the eXchange Calculus and executed using the FCPP C++ framework and simulator for AP. The tutorial combines conceptual foundations with practical guidance: participants learn how to specify spatio-temporal properties, generate corresponding monitors, and execute them in a 3D simulation environment. Examples are drawn from ongoing industrial collaborations and research projects, which we use to illustrate realistic monitoring scenarios and motivate open challenges for AP-based DRV.

Abstract Developing large-scale collective adaptive systems for safety-critical applications requires an extensive effort, involving the interplay of distributed programming techniques and mathematical proofs of real-time guarantees. This effort could be significantly reduced by allowing the system developer to rely on libraries of predefined algorithms. By exploiting such algorithms, distributed behaviour and (hard) real-time guarantees for the final application could be automatically inferred, effectively shifting the verification burden from the system designer to the algorithm developer. Following earlier work on real-time guarantees for aggregate computing algorithms, we argue that aggregate computing could provide a convenient framework towards this aim. As a first step, we give a detailed description of different kinds of models that can interpret corresponding classes of aggregate programs as mathematical functions. Then, building on such models, we investigate the problem of how real-time behaviour constraints can be specified in a compositional way, proposing a few composable specification patterns, and singling out a number of potential building block library algorithms that could constitute such a real-time aggregate computing library. We evaluate our proposal by means of examples, describing a series of example algorithms for each proposed model, and by investigating two possible compositions of some of them in an archetypal scenario of distributed estimation of the network diameter. In these two examples, we experimentally prove the effectiveness of the models by comparing the results of the interpretation with the simulations results, achieving a close match. Overall, the proposed framework provides a roadmap towards a real-time aggregate computing library with the potential of providing a valuable asset for supporting the rigorous engineering of safety-critical large-scale collective adaptive systems.

Recent trends like the Internet of Things (IoT) suggest a vision of dense and multi-scale deployments of computing devices in nearly all kinds of environments. A prominent engineering challenge revolves around programming the collective adaptive behaviour of such computational ecosystems. This requires abstractions able to capture concepts like ensembles (dynamic groups of cooperating devices) and collective tasks (joint activities carried out by ensembles). In this work, we consider collections of devices interacting with neighbours and that execute in nearly-synchronised sense-compute-interact rounds, where the computation is given by a single program mapping sensing values and incoming messages to output and outcoming messages. To support programming whole computational collectives, we propose the abstraction of a distributed collective process, which can be used to define at once the ensemble formation logic and its collective task. We formalise the abstraction in the eXchange Calculus (XC), a core functional language based on neighbouring values (maps from neighbours to values) where state and interaction is handled through a single primitive, exchange, and provide a corresponding implementation in the FCPP language. Then, we exercise distributed collective processes using two case studies: multi-hop message propagation and distributed monitoring of spatial properties. Finally, we discuss the features of the abstraction and its suitability for different kinds of distributed computing applications.

Today’s distributed and pervasive computing addresses large-scale cyber-physical ecosystems, characterised by dense and large networks of devices capable of computation, communication and interaction with the environment and people. While most research focuses on treating these systems as ‘composites’ (i.e., heterogeneous functional complexes), recent developments in fields such as self-organising systems and swarm robotics have opened up a complementary perspective: treating systems as ‘collectives’ (i.e., uniform, collaborative and self-organising groups of entities). This article explores the motivations, state of the art and implications of this ‘collective computing paradigm’ in software engineering. In particular, it discusses its peculiar challenges, implied by characteristics like distribution, situatedness, large scale and cooperative nature. These challenges outline significant directions for future research in software engineering, touching on aspects such as macro-programming, collective intelligence, self-adaptive middleware, learning/synthesis of collective behaviour, human involvement, safety and security in collective cyber-physical ecosystems.

Recent research on collective adaptive systems and macro-programming has shown the importance of programming abstractions for expressing the self-organising behaviour of ensembles, large and dynamic sets of collaborating devices. These generally leverage the interplay between the execution model and the program logic to steer the global-level emergent behaviour of the system. One notable example is the aggregate process abstraction: in an asynchronous round-based computational model, it allows to specify how aggregate-level computations are spawned, take form or spread on a domain of devices, and ultimately quit. Previous presentations of aggregate processes, however, are given in the formal framework of the field calculus, requiring knowledge of its syntax and articulated semantics. To provide a more accessible and language-agnostic presentation of such an abstraction, in this paper we introduce a general formal framework of collective computational processes (CCP). Specifically, as key contribution, we model and describe the programming interface (spawn construct) and dynamics of CCPs on event structures. Furthermore, we also propose novel algorithms for efficient propagation and termination of CCPs, based on statistics on the information speed and a notion of progressive wave-like closure. Crucially, thanks to our theoretical framework, we can provide optimality guarantees for the proposed algorithms, whose performance, superior to the state of the art, is assessed by simulation. Finally, to show applicability of CCPs, we provide a case study of situated service discovery in peer-to-peer networks.

Distributed collective systems are systems formed by homogeneous dynamic collections of devices acting in a shared environment to pursue a joint task or goal. Typical applications emerge in the context of wireless sensor networks, robot swarms, groups of wearable-augmented people, and computing infrastructures. Programming such systems is notoriously hard, due to requirements of scalability, concurrency, faults, and difficulty in making desired collective behaviour ultimately emerge: ad-hoc languages and mechanisms have been proposed threads like spatial computing, macro-programming, and field-based coordination. In this paper we present the eXchange Calculus (XC), formalising a tiny set of key mechanisms, usable across many different languages and platforms, allowing to express the overall interactive behaviour of distributed collective systems in a declarative way. In this approach, computation (executed in asynchronous rounds), communication (which is neighbour-based), and state over time, are all expressed by a single declarative construct, called exchange. We provide a formalisation of XC in terms of syntax, device-level and network-level semantics, prove a number of properties of the calculus, and discuss applicability considering a smart city scenario. XC is implemented as a DSL in Scala and in C＋＋, with different trade-offs in terms of productivity and platform targetting.

Recent works in contexts like the Internet of Things (IoT) and large-scale Cyber-Physical Systems (CPS) propose the idea of programming distributed systems by focussing on their global behaviour across space and time. In this view, a potentially vast and heterogeneous set of devices is considered as an "aggregate" to be programmed as a whole, while abstracting away the details of individual behaviour and exchange of messages, which are expressed declaratively. One such a paradigm, known as aggregate programming, builds on computational models inspired by field-based coordination. Existing models such as the field calculus capture interaction with neighbours by a so-called "neighbouring field" (a map from neighbours to values). This requires ad-hoc mechanisms to smoothly compose with standard values, thus complicating programming and introducing clutter in aggregate programs, libraries and domain-specific languages (DSLs). To address this key issue we introduce the novel notion of "computation against a neighbour", whereby the evaluation of certain subexpressions of the aggregate program are affected by recent corresponding evaluations in neighbours. We capture this notion in the neighbours calculus (NC), a new field calculus variant which is shown to smoothly support declarative specification of interaction with neighbours, and correspondingly facilitate the embedding of field computations as internal DSLs in common general-purpose programming languages -- as exemplified by a Scala implementation, called ScaFi. This paper formalises NC, thoroughly compares it with respect to the classic field calculus, and shows its expressiveness by means of a case study in edge computing, developed in ScaFi.

As the density of nodes capable of sensing, computing and actuation increases, it becomes increasingly useful to model an entire network of physical devices as a single, continuous space-time computing machine. The emergent behaviour of the whole software system is then induced by local computations deployed within each node and by the dynamics of the information diffusion. A relevant example of this distribution model is given byaggregate programmingand its minimal set of functional constructs used to manipulate distributed data structures evolving over space and time, and resulting in robustness to changes. In this paper, we propose the first implementation of the aggregate computing paradigm targeting microcontrollers, by integrating FCPP, a C++ implementation of the paradigm, with Miosix, a modern operating system for microcontrollers with full C++ support. To the best of the author's knowledge, we are the first to present results on the effectiveness of FCPP in an embedded operating system setting as opposed to a simulation environment, thus considering tight memory and computational constraints and accounting for packet losses due to nonidealities of the radio channel. We implemented and tested on a network of WandStem nodes two benchmark applications: a network connectivity checker for network planning and preventive maintenance, and a decentralised contact tracing application. Additionally, we show that common problems in sensor networks such as neighbour discovery, construction of a graph of the network topology, coarse grain clock synchronisation as well as network monitoring and the collection of statistics (such as memory occupation data) can be easily performed thanks to the expressive semantics of aggregate programming.

The complexity of large-scale distributed systems, particularly when deployed in physical space, calls for new mechanisms to address composability and reusability of collective adaptive behaviour. Computational fields have been proposed as an effective abstraction to fill the gap between the macro-level of such systems (specifying a system’s collective behaviour) and the micro-level (individual devices’ actions of computation and interaction to implement that collective specification), thereby providing a basis to better facilitate the engineering of collective APIs and complex systems at higher levels of abstraction. This article proposes a full formal foundation for field computations, in terms of a core (higher-order) calculus of computational fields containing a few key syntactic constructs, and equipped with typing, denotational and operational semantics. Critically, this allows formal establishment of a link between the micro- and macro-levels of collective adaptive systems by a result of computational adequacy and abstraction for the (aggregate) denotational semantics with respect to the (per-device) operational semantics.

As the density of sensing/computation/actuation nodes is increasing, it becomes more and more feasible and useful to think at an entire network of physical devices as a single, continuous space-time computing machine. The emergent behaviour of the whole software system is then induced by local computations deployed within each node and by the dynamics of the information diffusion. A relevant example of this distribution model is given by aggregate computing and its companion language field calculus, a minimal set of purely functional constructs used to manipulate distributed data structures evolving over space and time, and resulting in robustness to changes. In this paper, we study the convergence time of an archetypal and widely used component of distributed computations expressed in field calculus, called gradient: a fully-distributed estimation of distances over a metric space by a spanning tree. We provide an analytic result linking the quality of the output of a gradient to the amount of computing resources dedicated. The resulting error bounds are then exploited for network design, suggesting an optimal density value taking broadcast interferences into account. Finally, an empirical evaluation is performed validating the theoretical results.

Abstract We introduce the notion of ${\cal C}$ -system of filters, generalizing the standard definitions of both extenders and towers of normal ideals. This provides a framework to develop the theory of extenders and towers in a more general and concise way. In this framework we investigate the topic of definability of generic large cardinals properties.

We consider the problem of allocating N uniform data to K transmission channels so as the average Expected Delay (AED) is minimized. This problem arises in designing efficient data-diffusion broadcast algorithms in a smart environment. We show that the basic dynamic rogramming algorithm for solving the uniform pallocation problem can be speedup up to O(NK) time by applying an optimal algorithm to find the row-minima of totally monotone matrices. Such a new algorithm is always faster than the best previously known algorithm for the uniform allocation problem that runs in O(NKlogN). Moreover, it is computationally optimal for the uniform allocation of up to N data and K channels. We then reduce the largest allocation problem, i.e., the subproblem with exactly N data and K channels, to the problem of finding a minimum weight K-link path in a particular directed acyclic graph. We also present two heuristics and we show by extended simulations their effectiveness in practical scenarios. Both the K-link path algorithm and the heuristics are much faster than O(NK). We then compare the behaviours of our algorithms on the online version of the allocation problem in which new single items are inserted for broadcast.

Hereditarily finite sets (sets which are finite and have only hereditarily finite sets as members) are basic mathematical and computational objects, and also stand at the basis of some programming languages. We solve an open problem proposed by Kirby in 2008 concerning a recurrence relation for the cardinality an of the n-th level of the adjunctive hierarchy of hereditarily finite sets; in this hierarchy, new sets are formed by the addition of a new single element drawn from the already existing sets to an already existing set. We also show that our results can be generalized to sets with atoms, or can be refined by rank, cardinality, or by the maximum level from where the new adjoined element is drawn. We also show that an satisfies the asymptotic formula an=C2n+O(C2n−1)⁠, for a constant C≈1.3399⁠, which is a too fast asymptotic growth for practical purposes. We thus propose a very natural variant of the adjunctive hierarchy, whose asymptotic behaviour we prove to be Θ(2n)⁠.