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.

Ecological Networks (ENs) are a way to describe the structures of existing real ecosystems and to plan their expansion, conservation and improvement.In this work, we present a model to represent the specifications for the local planning of ENs in a way that can support reasoning, e.g., to detect violations within new proposals of expansion, or to reason about improvements of the networks.Moreover, we describe an OWL ontology for the representation of ENs themselves.In the context of knowledge engineering, ENs provide a complex, inherently geographic domain that demands for the expressive power of a language like OWL augmented with the GeoSPARQL ontology to be conveniently represented.More importantly, the set of specification rules that we consider (taken from the project for a local EN implementation) constitute a challenging problem for representing constraints over complex geographic domains, and evaluating whether a given large knowledge base satisfies or violates them.

It is well known that the problem of finding a feasible schedule for a partially ordered set of tasks can be formulated as a Disjunctive Temporal Problem (DTP). In case we want to find a schedule by taking preferences into account, there exist extensions to DTPs that augment them by associating numeric costs to the violation of individual temporal constraints, however, such extensions make the restrictive assumption that the costs associated with constraints are independent of one another. In this paper we propose a further extension, which enables the designer to specify (directional) dependencies between the preferences associated with the constraints. Such preferences are represented by exploiting Utility Difference Networks (UDNs), that define objective functions whose structure reflects conditional independencies among the nodes of the network. The paper describes the branch-and-bound algorithm at the core of the scheduling tool we have implemented for solving this new class of problems. We also present and discuss encouraging experimental results collected in two different test domains.

Several explanation and interpretation tasks, such as diagnosis, plan recognition and image interpretation, can be formalized as abductive reasoning. A number of approaches, including recent ones [1, 4], address the problem based on a task-independent representation of a domain which includes an ontology or taxonomy of hypotheses. In this paper we adopt a similar representation, but we also deal with abduction as an iterative process where, like in model-based diagnosis, further observations are proposed to discriminate among candidate explanations; in addition, we take into account costs of observations and actions. In fact, discrimination also involves refining hypotheses, but this is performed down to an appropriate level which depends on the cost of actions (e.g. repair actions or therapy) to be taken based on the results of abduction, and on the cost of additional observations, which should be balanced with the benefits, in terms of more suitable actions, of better discrimination. The presence of a domain representation with abstractions has a significant impact on this trade-off. In general, a better assessment of the situation at hand, based on additional observations, leads to a more focused action. However, the cost of observing the same phenomenon at different levels of abstraction may vary significantly; in fact, it could involve more or less costly medical or technical tests, or computationally complex image processing, possibly with additional costs due to the delay before taking an action. Moreover, the knowledge base could have been designed independently of the explanation/action task (e.g. diagnosis and repair), and could therefore include a detailed description of the domain which is not necessary for the task; more generally, the convenience of a detailed discrimination may depend on the specific case at hand. By explicitly considering abstractions in the iterative abduction process, we can often reduce the observation costs significantly, yet maintaining the ability to exploit detailed observations and knowledge when convenient (similar advantages have been shown in inductive classification with abstractions, e.g. [6]). In the following, we first describe the knowledge we expect to be available. We then describe a basic iterative abduction loop and, finally, we concentrate on the criterion for selecting the next step in the loop: either performing a next observation at some level of detail, or stopping because the estimated most convenient choice is performing the action(s) associated with the current hypotheses.

The paper addresses the problem of finding a compact representation of the diagnoses within a model-based approach to diagnosis. To this end, we introduce the notion of scenario, a special kind of CNF formula over the component variables, which can be used to encode a large number of diagnoses using the same amount of space needed for encoding just a single diagnosis. We show how the solutions to a diagnostic problem can be computed as sets of scenarios by presenting first an exhaustive algorithm and then an efficient algorithm, which exploits probabilistic information to restrict the result set to preferred scenarios. Finally, we discuss the issue of how to efficiently extract preferred diagnoses from sets of scenarios and characterize a class of system models for which our techniques perform particularly well. Concepts and algorithms introduced in the paper have been tested within the prototype of the diagnostic agent of a space robotic arm; resulting statistics are reported and critically discussed.