Author name cluster

Ferruccio Damiani

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

8 papers

1 author row

FM Conference 2026 Conference Paper

Distributed Runtime Verification in Proximity-Based Networks: A Tutorial on the Aggregate Programming Approach

Giorgio Audrito
Ferruccio Damiani
Giordano Scarso
Volker Stolz
Gianluca Torta

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.

DOI

TCS Journal 2022 Journal Article

On logical and extensional characterizations of attributed feature models

Ferruccio Damiani
Michael Lienhardt
Luca Paolini

Software-intensive systems can have thousands of interdependent configuration options across different subsystems. Feature models (FMs) allow designers to organize the configuration space by describing configuration options using interdependent features: a feature is a name representing some functionality and each software variant is identified by a set of features. Attributed feature models (AFMs) extend FMs to describe the, possibly constrained, choice of a value from domains such as integers or strings: each attribute is associated to one feature, and when the feature is selected then the attribute brings some additional information relative to the selected features. Different representations of FMs and AFMs have been proposed in the literature. In this paper we focus on the logical representation (which works well in practice) and the extensional representation (which has been recently shown well suited for theoretical investigations). We provide an algebraic and a logical characterization of operations and relations on FMs and AFMs, and we formalize the connection between the two characterizations as monomorphisms from lattices of logical FMs and AFMs to lattices of extensional FMs and AFMs, respectively. This formalization sheds new light on the correspondence between the algebraic and logical characterizations of operations and relations for FMs and AFMs. It aims to foster the development of a formal framework for supporting practical exploitation of future theoretical developments on FMs, AFMs and multi software product lines.

Details DOI

EAAI Journal 2021 Journal Article

Engineering collective intelligence at the edge with aggregate processes

Roberto Casadei
Mirko Viroli
Giorgio Audrito
Danilo Pianini
Ferruccio Damiani

Edge computing promotes the execution of complex computational processes without the cloud, i. e. , on top of the heterogeneous, articulated, and possibly mobile systems composed of IoT and edge devices. Such a pervasive smart fabric augments our environment with computing and networking capabilities. This leads to a complex and dynamic ecosystem of devices that should not only exhibit individual intelligence but also collective intelligence—the ability to take group decisions or process knowledge among autonomous units of a distributed environment. Self-adaptation and self-organisation mechanisms are also typically required to ensure continuous and inherent toleration of changes of various kinds, to distribution of devices, energy available, computational load, as well as faults. To achieve this behaviour in a massively distributed setting like edge computing demands, we seek for identifying proper abstractions, and engineering tools therefore, to smoothly capture collective behaviour, adaptivity, and dynamic injection and execution of concurrent distributed activities. Accordingly, we elaborate on a notion of “aggregate process” as a concurrent collective computation whose execution and interactions are sustained by a dynamic team of devices, whose spatial region can opportunistically vary over time. We ground this notion by extending the aggregate computing model and toolchain with new constructs to instantiate aggregate processes and regulate key aspects of their lifecycle. By virtue of an open-source implementation in the ScaFi framework, we show basic programming examples as well as case studies of edge computing, evaluated by simulation in realistic settings.

Details DOI

AAMAS Conference 2019 Conference Paper

Effective Collective Summarisation of Distributed Data in Mobile Multi-Agent Systems

Giorgio Audrito
Sergio Bergamini
Ferruccio Damiani
Mirko Viroli

One of the key applications of physically-deployed multi-agent systems, such as mobile robots, drones, or personal agents in human mobility scenarios, is to promote a pervasive notion of distributed sensing achieved by strict agent cooperation. A quintessential operation of distributed sensing is data summarisation over a region of space, which finds many applications in variations of counting problems: counting items, measuring space, averaging environmental values, and so on. A typical strategy to perform peer-to-peer data summarisation with local interactions is to progressively accumulate information towards one or more collector agents, though this typically exhibits several sources of fragility, especially in scenarios featuring high mobility. In this paper, we introduce a new multi-agent algorithm for dynamic summarisation of distributed data, called parametric weighted multi-path, based on a local strategy to break, send, and then recombine sensed data across neighbours based on their estimated distance, ultimately resulting in the formation of multiple, dynamic and emergent paths of information flow towards collectors. By empirical evaluation via simulation in synthetic and realistic case studies, accounting for various sources of volatility, using different state-of-the-art distance estimations, and comparing to other existing implementations of aggregation algorithms, we show that parametric weighted multi-path is able to retain adequate accuracy even in high-variability scenarios where all other algorithms are significantly diverging from correct estimations.

PDF

TAAS Journal 2017 Journal Article

Self-Adaptation to Device Distribution in the Internet of Things

Jacob Beal
Mirko Viroli
Danilo Pianini
Ferruccio Damiani

A key problem when coordinating the behaviour of spatially situated networks, like those typically found in the Internet of Things (IoT), is adaptation to changes impacting network topology, density, and heterogeneity. Computational goals for such systems, however, are often dependent on geometric properties of the continuous environment in which the devices are situated rather than the particulars of how devices happen to be distributed through it. In this article, we identify a new property of distributed algorithms, eventual consistency, which guarantees that computation converges to a final state that approximates a predictable limit, based on the continuous environment, as the density and speed of devices increases. We then identify a large class of programs that are eventually consistent, building on prior results on the field calculus computational model (Beal et al. 2015; Viroli et al. 2015a) that identify a class of self-stabilizing programs. Finally, we confirm through simulation of IoT application scenarios that eventually consistent programs from this class can provide resilient behavior where programs that are only converging fail badly.

Details DOI

TCS Journal 2012 Journal Article

Simulation techniques for the calculus of wrapped compartments

Mario Coppo
Ferruccio Damiani
Maurizio Drocco
Elena Grassi
Eva Sciacca
Salvatore Spinella
Angelo Troina

The modelling and analysis of biological systems has deep roots in Mathematics, specifically in the field of Ordinary Differential Equations (ODEs). Alternative approaches based on formal calculi, often derived from process algebras or term rewriting systems, provide a quite complementary way to analyse the behaviour of biological systems. These calculi allow to cope in a natural way with notions like compartments and membranes, which are not easy (sometimes impossible) to handle with purely numerical approaches, and are often based on stochastic simulation methods. Recently, it has also become evident that stochastic effects in regulatory networks play a crucial role in the analysis of such systems. Actually, in many situations it is necessary to use stochastic models. For example when the system to be described is based on the interaction of few molecules, when we are at the presence of a chemical instability, or when we want to simulate the functioning of a pool of entities whose compartmentalised structure evolves dynamically. In contrast, stable metabolic networks, involving a large number of reagents, for which the computational cost of a stochastic simulation becomes an insurmountable obstacle, are efficiently modelled with ODEs. In this paper we define a hybrid simulation method, combining the stochastic approach with ODEs, for systems described in the Calculus of Wrapped Compartments (CWC), a calculus on which we can express the compartmentalisation of a biological system whose evolution is defined by a set of rewrite rules.

Details DOI

GandALF Workshop 2011 Workshop Paper

Type Inference for Bimorphic Recursion

Makoto Tatsuta
Ferruccio Damiani

This paper proposes bimorphic recursion, which is restricted polymorphic recursion such that every recursive call in the body of a function definition has the same type. Bimorphic recursion allows us to assign two different types to a recursively defined function: one is for its recursive calls and the other is for its calls outside its definition. Bimorphic recursion in this paper can be nested. This paper shows bimorphic recursion has principal types and decidable type inference. Hence bimorphic recursion gives us flexible typing for recursion with decidable type inference. This paper also shows that its typability becomes undecidable because of nesting of recursions when one removes the instantiation property from the bimorphic recursion.

PDF Details DOI

TCS Journal 2002 Journal Article

Strictness, totality, and non-standard-type inference

Mario Coppo
Ferruccio Damiani
Paola Giannini

In this paper we present two non-standard-type inference systems for conjunctive strictness and totality analyses of higher-order-typed functional programs and prove completeness results for both the strictness and the totality-type entailment relations. We also study the interactions between strictness and totality analyses, showing that the information obtainable by a system that combines the two analyses, even though more refined than the information given by the two separate systems, cannot be effectively used. A main feature of our approach is that all the results are proved by relying directly on the operational semantics of the programming language considered. This leads to a rather direct presentation which involves relatively little mathematical overhead.

Details DOI