According to Kings Research [1] the global Wearable Market is projected to reach US$ 192.14 billion by 2030, growing at a CAGR of 15.8% from 2023 to 2030, with an increasing growth caused by the COVID-19. The industry and public sector are then pushing for innovative WCS solutions with high levels of dependability and trustworthiness that can efficiently operate in increasingly complex scenarios. Great strides have been made to realize WCS for the 24/7 monitoring of single users based on 3-tier architectures involving wearables, edge, and cloud systems. However, new requirements targeting cooperative multiuser scenarios demand radically new approaches, as promoted by the community-oriented WCS (CO-WCS). The COMMON-WEARS project is developing novel models and architectures for next-generation CO-WCS, defining a rigorous engineering methodology, with associated formal verification and simulation tools, to drive the development lifecycle of CO-WCS and creating a pilot in a real instrumented environment to support activities of surgical teams in operating rooms. COMMON-WEARS strives to move the research front by developing CO-WCS featuring multi-user collectives of smart wearables and body sensor networks (BSN), with applications, e.g., in domestic, urban, manufacturing, emergency, and working environments. This is achieved by combining aggregate computing, collective opportunistic IoT, machine learning, and WCS/BSN architectures. Herein, we discuss lessons learned from prototyping new concepts in collaborative wearable computing, in the contest of challenging use cases, including healthcare, emergency response and pandemic management, which are strongly impacted by smart wearables.

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.

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.

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.

Proof Theory and Type Theory are two branches of mathematical logic and theoretical computer science that explore the structure of mathematical proofs and the foundations of computation. Both are crucial for understanding formal systems, programming languages, and constructive mathematics. Stefano Berardi is an influential researcher in these fields, particularly known for his work on constructive logic, dependent types, and more recently, cyclic proofs. These proceedings intend to collect papers by researchers who are active in the field and often have been coauthors of Stefano, aimed to illustrate the achievements and the perspectives of this research area.

In this paper we: (1) propose Lightweight C (LC), namely a core calculus that formalizes a proper subset of the ANSI C without preprocessor directives; (2) define Colored LC (CLC), namely LC endowed with ANSI C preprocessor directives; and (3) define a type system for CLC that guarantees that all programs to be generated by the C preprocessor are well-typed C programs. We believe that the simple formalization provided by CLC could be useful also for teaching purposes. Stefano Berardi spent most of his academic career at the Department of Computer Science of the University of Turin, where he conducts outstanding research on the logical foundations of computer science and on type-based program analyses. Over the years, he taught many courses, from BSc courses on programming with C to PhD courses on program analysis. Therefore, this paper fully falls within Stefano Berardi's research and teaching activities.

Aggregate Programming (AP) is a paradigm for programming the collective behaviour of sets of distributed devices, possibly situated at the network far edge, by relying on asynchronous proximity-based interactions. The eXchange Calculus (XC), a recently proposed foundational model for AP, is essentially a typed lambda calculus extended with an operator (the exchange operator) providing an implicit communication mechanism between neighbour devices. This paper provides a gentle introduction to XC and to its implementation as a C++ library, called FCPP. The FCPP library and toolchain has been mainly developed at the Department of Computer Science of the University of Turin, where Stefano Berardi spent most of his academic career conducting outstanding research about logical foundation of computer science and transmitting his passion for research to students and young researchers, often exploiting typed lambda calculi. An FCCP program is essentially a typed lambda term, and FCPP has been used to write code that has been deployed on devices at the far edge of the network, including rovers and (soon) Uncrewed Aerial Vehicles (UAVs); hence the title of the paper.

Multi-robot systems are becoming increasingly relevant within diverse application domains, such as healthcare, exploration, and rescue missions. However, building such systems is still a significant challenge, since it adds the complexities of the physical nature of robots and their environments to those inherent in coordinating any distributed (multi-agent) system. Aggregate Programming (AP) has recently emerged as a promising approach to engineering resilient, distributed systems with proximity-based communication, and is notably supported by practical frameworks. In this paper we present a prototype of a multi-robot service system, which adopts AP for the design and implementation of its coordination software. The prototype has been validated both with simulations, and with tests in a University library.

Self-adaptation, meant to increase reliability, is a crucial feature of cyber-physical systems operating in uncertain physical environments. Ensuring safety properties of self-adaptive systems is of utter importance, especially when operating in remote environments where communication with a human operator is limited, like under water or in space. This paper presents a software model that allows the analysis of one such self-adaptive system, a configurable underwater robot used for pipeline inspection, by means of the probabilistic model checker ProFeat. Furthermore, it shows that the configurable software model is easily extensible to further, possibly more complex use cases and analyses.

This one-page document summarises a paper published in FAC [1].

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.

Community-oriented wearable computing systems, where interconnected wearable devices act collectively to provide community-wide services, are increasingly used in healthcare scenarios where reliable monitoring and coordination are crucial. This paper investigates the feasibility of applying aggregate runtime verification techniques to ensure safety in such systems, particularly during large-scale crowded events where connectivity is limited. Our approach leverages aggregate programming, a distributed macroprogramming paradigm that enables verification of system-wide properties without central control or data collection. Through a case study on emergency healthcare, we demonstrate how this framework can detect emergencies and trigger appropriate responses in a fully distributed manner, addressing challenges in connectivity and safety.

In Machine Learning (ML), the deployment of complex Neural Network (NN) models on memory-constrained Internet of Things (IoT) devices presents a significant challenge. Tiny Machine Learning (TinyML) focuses on optimizing NN models for such environments, where computational and storage resources are limited. A major aspect of this optimization involves reducing model size without substantially compromising accuracy. We conducted a systematic literature review to identify pruning and quantization techniques suitable for optimization of NN models. In addition, this study investigates the efficiency of pruning and 8-bit integer (INT8) quantization in optimizing NN models for deployment on memory-constrained devices. The study evaluates widely used NN architectures such as ResNet50/101, VGG16, and MobileNet, alongside a custom-designed model, using CIFAR-100, CIFAR-10, MNIST, and Fashion-MNIST datasets. The results show that combining pruning with INT8 quantization reduced the size of MobileNet by 77.01

This one-page document summarises a paper published in JSS [1].

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.

In object-oriented languages, dynamic object reclassification is a technique to change the class binding of an object at runtime. Current approaches express when and how to reclassify inside the program's business code, while maintaining internal consistency. These approaches are less suited for programs that need to be consistent with an external context, such as autonomous systems interacting with a knowledge base. This paper proposes declarative dynamic object reclassification, a novel technique that provides a separation of concerns between a program's business code and its adaptation logic for reclassification, expressed via a knowledge base. We present Featherweight Semantically Reflected Java, a minimal calculus for declarative dynamic object reclassification that enables the programmer to define consistency both internally (using a type system) and externally (using declarative classification queries). We use this calculus to study how internal and external consistency interact for declarative dynamic object reclassification. We further implement the technique by extending SMOL, a language for reflective programming via external knowledge bases.

Self-organisation and collective adaptation are highly desired features for several kinds of large-scale distributed systems including robotic swarms, computational ecosystems, wearable collectives, and Internet-of-Things systems. These kinds of distributed processes, addressing functional and non-functional aspects of complex socio-technical systems, can emerge in an engineered/controlled way from (re)active decentralised activity and interaction across all physical and logical system devices. In this work, we study how the Actors programming model can be adopted to support collective self-organising behaviours. Specifically, we analyse the features of the Actors model, such as reactivity, asynchrony, and locality, that are instrumental for implementing the adaptive coordination of large-scale systems, and discuss potential actor-based designs, from simple ad-hoc implementation of algorithms to a full-fledged general toolkit. In particular, the approach is incarnated in the aggregate computing paradigm, which stands as a comprehensive engineering approach for self-organisation. This is based on Akka, and can be fully programmed in the Scala programming language thanks to the ScaFi aggregate computing toolkit.