-
Optimizing Fault-Tolerant Quality-Guaranteed Sensor Deployments for UAV Localization in Critical Areas via Computational Geometry
Authors:
Marco Esposito,
Toni Mancini,
Enrico Tronci
Abstract:
The increasing spreading of small commercial Unmanned Aerial Vehicles (UAVs, aka drones) presents serious threats for critical areas such as airports, power plants, governmental and military facilities. In fact, such UAVs can easily disturb or jam radio communications, collide with other flying objects, perform espionage activity, and carry offensive payloads, e.g., weapons or explosives. A centra…
▽ More
The increasing spreading of small commercial Unmanned Aerial Vehicles (UAVs, aka drones) presents serious threats for critical areas such as airports, power plants, governmental and military facilities. In fact, such UAVs can easily disturb or jam radio communications, collide with other flying objects, perform espionage activity, and carry offensive payloads, e.g., weapons or explosives. A central problem when designing surveillance solutions for the localization of unauthorized UAVs in critical areas is to decide how many triangulating sensors to use, and where to deploy them to optimise both coverage and cost effectiveness.
In this article, we compute deployments of triangulating sensors for UAV localization, optimizing a given blend of metrics, namely: coverage under multiple sensing quality levels, cost-effectiveness, fault-tolerance. We focus on large, complex 3D regions, which exhibit obstacles (e.g., buildings), varying terrain elevation, different coverage priorities, constraints on possible sensors placement. Our novel approach relies on computational geometry and statistical model checking, and enables the effective use of off-the-shelf AI-based black-box optimizers. Moreover, our method allows us to compute a closed-form, analytical representation of the region uncovered by a sensor deployment, which provides the means for rigorous, formal certification of the quality of the latter.
We show the practical feasibility of our approach by computing optimal sensor deployments for UAV localization in two large, complex 3D critical regions, the Rome Leonardo Da Vinci International Airport (FCO) and the Vienna International Center (VIC), using NOMAD as our state-of-the-art underlying optimization engine. Results show that we can compute optimal sensor deployments within a few hours on a standard workstation and within minutes on a small parallel infrastructure.
△ Less
Submitted 5 December, 2023;
originally announced December 2023.
-
Optimising Highly-Parallel Simulation-Based Verification of Cyber-Physical Systems
Authors:
Toni Mancini,
Igor Melatti,
Enrico Tronci
Abstract:
Cyber-Physical Systems (CPSs), comprising both software and physical components, arise in many industry-relevant domains and are often mission- or safety-critical.
System-Level Verification (SLV) of CPSs aims at certifying that given (e.g., safety or liveness) specifications are met, or at estimating the value of some KPIs, when the system runs in its operational environment, i.e., in presence o…
▽ More
Cyber-Physical Systems (CPSs), comprising both software and physical components, arise in many industry-relevant domains and are often mission- or safety-critical.
System-Level Verification (SLV) of CPSs aims at certifying that given (e.g., safety or liveness) specifications are met, or at estimating the value of some KPIs, when the system runs in its operational environment, i.e., in presence of inputs (from users or other systems) and/or of additional, uncontrolled disturbances.
To enable SLV of complex systems from the early design phases, the currently most adopted approach envisions the simulation of a system model under the (time bounded) operational scenarios of interest. Simulation-based SLV can be computationally prohibitive (years of sequential simulation), since model simulation is computationally intensive and the set of scenarios of interest can huge.
We present a technique that, given a collection of scenarios of interest (extracted from mass-storage databases or from symbolic structures, e.g., constraint-based scenario generators), computes parallel shortest simulation campaigns, which drive a possibly large number of system model simulators running in parallel in a HPC infrastructure through all (and only) those scenarios in the user-defined (possibly random) order, by wisely avoiding multiple simulations of repeated trajectories, thus minimising the overall completion time, compatibly with the available simulator memory capacity.
Our experiments on Modelica/FMU and Simulink case study models with up to ~200 million scenarios show that our optimisation yields speedups as high as 8x. This, together with the enabled massive parallelisation, makes practically viable (a few weeks in a HPC infrastructure) verification tasks (both statistical and exhaustive, with respect to the given set of scenarios) which would otherwise take inconceivably long time.
△ Less
Submitted 28 July, 2023;
originally announced July 2023.
-
High Sensitivity real-time VOCs monitoring in air through FTIR Spectroscopy using a Multipass Gas Cell Setup
Authors:
A. D'Arco,
T. Mancini,
M. C. Paolozzi,
S. Macis,
A. Marcelli,
M. Petrarca,
F. Radica,
G. Tranfo,
S. Lupi,
G. della Ventura
Abstract:
Human exposure to Volatile Organic Compounds (VOCs) and their presence in indoor and working environments is recognized as a serious health risk, causing impairment of varying severity. Different detecting systems able to monitor VOCs are available in the market, however they have significant limitations for both sensitivity and chemical discrimination capability. During the last years we studied…
▽ More
Human exposure to Volatile Organic Compounds (VOCs) and their presence in indoor and working environments is recognized as a serious health risk, causing impairment of varying severity. Different detecting systems able to monitor VOCs are available in the market, however they have significant limitations for both sensitivity and chemical discrimination capability. During the last years we studied systematically the use of Fourier Transform Infrared Spectroscopy (FTIR) spectroscopy as an alternative, powerful tool for quantifying VOCs in air. We calibrated the method for a set of compounds (styrene, acetone, ethanol and isopropanol) by using both laboratory and portable infrared spectrometers. The aim was to develop a new, real time and highly sensitive sensor system for VOCs monitoring. In this paper, we improve the setup performance testing the feasibility of using a multipass cell with the aim of extending the sensitivity of this sensor system down to the part per milion (ppb) level. Considering that multipass cells are now available also for portable instruments, this study opens the road for the design of new high-resolution devices for environmental monitoring.
△ Less
Submitted 1 July, 2022;
originally announced July 2022.
-
Any-horizon uniform random sampling and enumeration of constrained scenarios for simulation-based formal verification
Authors:
Toni Mancini,
Igor Melatti,
Enrico Tronci
Abstract:
Model-based approaches to the verification of non-terminating Cyber-Physical Systems (CPSs) usually rely on numerical simulation of the System Under Verification (SUV) model under input scenarios of possibly varying duration, chosen among those satisfying given constraints. Such constraints typically stem from requirements (or assumptions) on the SUV inputs and its operational environment as well…
▽ More
Model-based approaches to the verification of non-terminating Cyber-Physical Systems (CPSs) usually rely on numerical simulation of the System Under Verification (SUV) model under input scenarios of possibly varying duration, chosen among those satisfying given constraints. Such constraints typically stem from requirements (or assumptions) on the SUV inputs and its operational environment as well as from the enforcement of additional conditions aiming at, e.g., prioritising the (often extremely long) verification activity, by, e.g., focusing on scenarios explicitly exercising selected requirements, or avoiding vacuity in their satisfaction. In this setting, the possibility to efficiently sample at random (with a known distribution, e.g., uniformly) within, or to efficiently enumerate (possibly in a uniformly random order) scenarios among those satisfying the given constraints is a key enabler for the viability of the verification process, e.g., via simulation-based statistical model checking. Unfortunately, in case of non-trivial combinations of constraints, iterative approaches like Markovian random walks in the space of sequences of inputs in general fail in extracting scenarios according to a given distribution, and can be very inefficient to produce legal scenarios of interest. We show how, given a set of constraints on the input scenarios succinctly defined by finite memory monitors, a data structure (scenario generator) can be synthesised, from which any-horizon scenarios satisfying the input constraints can be efficiently extracted by (possibly uniform) random sampling or (randomised) enumeration. Our approach enables seamless support to virtually all simulation-based approaches to CPS verification, ranging from simple random testing to statistical model checking and formal (i.e., exhaustive) verification.
△ Less
Submitted 6 September, 2021;
originally announced September 2021.
-
A Two-Layer Near-Optimal Strategy for Substation Constraint Management via Home Batteries
Authors:
Igor Melatti,
Federico Mari,
Toni Mancini,
Milan Prodanovic,
Enrico Tronci
Abstract:
Within electrical distribution networks, substation constraints management requires that aggregated power demand from residential users is kept within suitable bounds. Efficiency of substation constraints management can be measured as the reduction of constraints violations w.r.t. unmanaged demand. Home batteries hold the promise of enabling efficient and user-oblivious substation constraints mana…
▽ More
Within electrical distribution networks, substation constraints management requires that aggregated power demand from residential users is kept within suitable bounds. Efficiency of substation constraints management can be measured as the reduction of constraints violations w.r.t. unmanaged demand. Home batteries hold the promise of enabling efficient and user-oblivious substation constraints management. Centralized control of home batteries would achieve optimal efficiency. However, it is hardly acceptable by users, since service providers (e.g., utilities or aggregators) would directly control batteries at user premises. Unfortunately, devising efficient hierarchical control strategies, thus overcoming the above problem, is far from easy.
We present a novel two-layer control strategy for home batteries that avoids direct control of home devices by the service provider and at the same time yields near-optimal substation constraints management efficiency. Our simulation results on field data from 62 households in Denmark show that the substation constraints management efficiency achieved with our approach is at least 82% of the one obtained with a theoretical optimal centralized strategy.
△ Less
Submitted 15 August, 2021;
originally announced August 2021.
-
Parallel Statistical Model Checking for Safety Verification in Smart Grids
Authors:
T. Mancini,
F. Mari,
I. Melatti,
I. Salvo,
E. Tronci,
J. K. Gruber,
B. Hayes,
M. Prodanovic,
L. Elmegaard
Abstract:
By using small computing devices deployed at user premises, Autonomous Demand Response (ADR) adapts users electricity consumption to given time-dependent electricity tariffs. This allows end-users to save on their electricity bill and Distribution System Operators to optimise (through suitable time-dependent tariffs) management of the electric grid by avoiding demand peaks. Unfortunately, even wit…
▽ More
By using small computing devices deployed at user premises, Autonomous Demand Response (ADR) adapts users electricity consumption to given time-dependent electricity tariffs. This allows end-users to save on their electricity bill and Distribution System Operators to optimise (through suitable time-dependent tariffs) management of the electric grid by avoiding demand peaks. Unfortunately, even with ADR, users power consumption may deviate from the expected (minimum cost) one, e.g., because ADR devices fail to correctly forecast energy needs at user premises. As a result, the aggregated power demand may present undesirable peaks. In this paper we address such a problem by presenting methods and a software tool (APD-Analyser) implementing them, enabling Distribution System Operators to effectively verify that a given time-dependent electricity tariff achieves the desired goals even when end-users deviate from their expected behaviour. We show feasibility of the proposed approach through a realistic scenario from a medium voltage Danish distribution network.
△ Less
Submitted 20 June, 2021;
originally announced June 2021.
-
MILP, pseudo-boolean, and OMT solvers for optimal fault-tolerant placements of relay nodes in mission critical wireless networks
Authors:
Quian Matteo Chen,
Alberto Finzi,
Toni Mancini,
Igor Melatti,
Enrico Tronci
Abstract:
In critical infrastructures like airports, much care has to be devoted in protecting radio communication networks from external electromagnetic interference. Protection of such mission-critical radio communication networks is usually tackled by exploiting radiogoniometers: at least three suitably deployed radiogoniometers, and a gateway gathering information from them, permit to monitor and locali…
▽ More
In critical infrastructures like airports, much care has to be devoted in protecting radio communication networks from external electromagnetic interference. Protection of such mission-critical radio communication networks is usually tackled by exploiting radiogoniometers: at least three suitably deployed radiogoniometers, and a gateway gathering information from them, permit to monitor and localise sources of electromagnetic emissions that are not supposed to be present in the monitored area. Typically, radiogoniometers are connected to the gateway through relay nodes. As a result, some degree of fault-tolerance for the network of relay nodes is essential in order to offer a reliable monitoring. On the other hand, deployment of relay nodes is typically quite expensive. As a result, we have two conflicting requirements: minimise costs while guaranteeing a given fault-tolerance. In this paper, we address the problem of computing a deployment for relay nodes that minimises the relay node network cost while at the same time guaranteeing proper working of the network even when some of the relay nodes (up to a given maximum number) become faulty (fault-tolerance). We show that, by means of a computation-intensive pre-processing on a HPC infrastructure, the above optimisation problem can be encoded as a 0/1 Linear Program, becoming suitable to be approached with standard Artificial Intelligence reasoners like MILP, PB-SAT, and SMT/OMT solvers. Our problem formulation enables us to present experimental results comparing the performance of these three solving technologies on a real case study of a relay node network deployment in areas of the Leonardo da Vinci Airport in Rome, Italy.
△ Less
Submitted 20 June, 2021;
originally announced June 2021.
-
Optimal personalised treatment computation through in silico clinical trials on patient digital twins
Authors:
Stefano Sinisi,
Vadim Alimguzhin,
Toni Mancini,
Enrico Tronci,
Federico Mari,
Brigitte Leeners
Abstract:
In Silico Clinical Trials (ISTC), i.e., clinical experimental campaigns carried out by means of computer simulations, hold the promise to decrease time and cost for the safety and efficacy assessment of pharmacological treatments, reduce the need for animal and human testing, and enable precision medicine. In this paper we present methods and an algorithm that, by means of extensive computer simul…
▽ More
In Silico Clinical Trials (ISTC), i.e., clinical experimental campaigns carried out by means of computer simulations, hold the promise to decrease time and cost for the safety and efficacy assessment of pharmacological treatments, reduce the need for animal and human testing, and enable precision medicine. In this paper we present methods and an algorithm that, by means of extensive computer simulation--based experimental campaigns (ISTC) guided by intelligent search, optimise a pharmacological treatment for an individual patient (precision medicine). e show the effectiveness of our approach on a case study involving a real pharmacological treatment, namely the downregulation phase of a complex clinical protocol for assisted reproduction in humans.
△ Less
Submitted 20 June, 2021;
originally announced June 2021.
-
SBML2Modelica: integrating biochemical models within open-standard simulation ecosystems
Authors:
Filippo Maggioli,
Toni Mancini,
Enrico Tronci
Abstract:
Motivation: SBML is the most widespread language for the definition of biochemical models. Although dozens of SBML simulators are available, there is a general lack of support to the integration of SBML models within open-standard general-purpose simulation ecosystems. This hinders co-simulation and integration of SBML models within larger model networks, in order to, e.g. enable in silico clinica…
▽ More
Motivation: SBML is the most widespread language for the definition of biochemical models. Although dozens of SBML simulators are available, there is a general lack of support to the integration of SBML models within open-standard general-purpose simulation ecosystems. This hinders co-simulation and integration of SBML models within larger model networks, in order to, e.g. enable in silico clinical trials of drugs, pharmacological protocols, or engineering artefacts such as biomedical devices against Virtual Physiological Human models. Modelica is one of the most popular existing open-standard general-purpose simulation languages, supported by many simulators. Modelica models are especially suited for the definition of complex networks of heterogeneous models from virtually all application domains. Models written in Modelica (and in 100+ other languages) can be readily exported into black-box Functional Mock-Up Units (FMUs), and seamlessly co-simulated and integrated into larger model networks within open-standard language-independent simulation ecosystems.
Results: In order to enable SBML model integration within heterogeneous model networks, we present SBML2Modelica, a software system translating SBML models into well-structured, user-intelligible, easily modifiable Modelica models. SBML2Modelica is SBML Level 3 Version 2-compliant and succeeds on 96.47% of the SBML Test Suite Core (with a few rare, intricate and easily avoidable combinations of constructs unsupported and cleanly signalled to the user). Our experimental campaign on 613 models from the BioModels database (with up to 5438 variables) shows that the major open-source (general-purpose) Modelica and FMU simulators achieve performance comparable to state-of-the-art specialized SBML simulators.
Availability and implementation: https://bitbucket.org/mclab/sbml2modelica
△ Less
Submitted 31 May, 2021;
originally announced June 2021.
-
Reconciling interoperability with efficient Verification and Validation within open source simulation environments
Authors:
Stefano Sinisi,
Vadim Alimguzhin,
Toni Mancini,
Enrico Tronci
Abstract:
A Cyber-Physical System (CPS) comprises physical as well as software subsystems. Simulation-based approaches are typically used to support design and Verification and Validation (V&V) of CPSs in several domains such as: aerospace, defence, automotive, smart grid and healthcare. Accordingly, many simulation-based tools are available, and this poses huge interoperability challenges. To overcome them…
▽ More
A Cyber-Physical System (CPS) comprises physical as well as software subsystems. Simulation-based approaches are typically used to support design and Verification and Validation (V&V) of CPSs in several domains such as: aerospace, defence, automotive, smart grid and healthcare. Accordingly, many simulation-based tools are available, and this poses huge interoperability challenges. To overcome them, in 2010 the Functional Mock-up Interface (FMI) was proposed as an open standard to support both Model Exchange (ME) and Co-Simulation (CS). Models adhering to such a standard are called Functional Mock-up Units (FMUs). FMUs play an essential role in defining complex CPSs through, e.g., the SSP standard. Simulation-based V&V of CPSs typically requires exploring different scenarios (i.e., exogenous CPS input sequences), many of them showing a shared prefix. Accordingly, the simulator state at the end of a shared prefix is saved and then restored and used as a start state for the simulation of the next scenario. In this context, an important FMI feature is the capability to save and restore the internal FMU state on demand. Unfortunately, the implementation of this feature is not mandatory and it is available only within some commercial software. This motivates develo** such a feature for open-source CPS simulation environments. In this paper, we focus on JModelica, an open-source modelling and simulation environment for CPSs defined in the Modelica language. We describe how we have endowed JModelica with our open-source implementation of the FMI 2.0 functions to save and restore internal states of FMUs for ME. Furthermore, we present results evaluating, through 934 benchmark models, correctness and efficiency of our extended JModelica. Our results show that simulation-based V&V is, on average, 22 times faster with our get/set functionality than without it.
△ Less
Submitted 31 May, 2021;
originally announced June 2021.
-
Prediction intervals for Deep Neural Networks
Authors:
Tullio Mancini,
Hector Calvo-Pardo,
Jose Olmo
Abstract:
The aim of this paper is to propose a suitable method for constructing prediction intervals for the output of neural network models. To do this, we adapt the extremely randomized trees method originally developed for random forests to construct ensembles of neural networks. The extra-randomness introduced in the ensemble reduces the variance of the predictions and yields gains in out-of-sample acc…
▽ More
The aim of this paper is to propose a suitable method for constructing prediction intervals for the output of neural network models. To do this, we adapt the extremely randomized trees method originally developed for random forests to construct ensembles of neural networks. The extra-randomness introduced in the ensemble reduces the variance of the predictions and yields gains in out-of-sample accuracy. An extensive Monte Carlo simulation exercise shows the good performance of this novel method for constructing prediction intervals in terms of coverage probability and mean square prediction error. This approach is superior to state-of-the-art methods extant in the literature such as the widely used MC dropout and bootstrap procedures. The out-of-sample accuracy of the novel algorithm is further evaluated using experimental settings already adopted in the literature.
△ Less
Submitted 13 May, 2021; v1 submitted 8 October, 2020;
originally announced October 2020.
-
Simulator Semantics for System Level Formal Verification
Authors:
Toni Mancini,
Federico Mari,
Annalisa Massini,
Igor Melatti,
Enrico Tronci
Abstract:
Many simulation based Bounded Model Checking approaches to System Level Formal Verification (SLFV) have been devised. Typically such approaches exploit the capability of simulators to save computation time by saving and restoring the state of the system under simulation. However, even though such approaches aim to (bounded) formal verification, as a matter of fact, the simulator behaviour is not f…
▽ More
Many simulation based Bounded Model Checking approaches to System Level Formal Verification (SLFV) have been devised. Typically such approaches exploit the capability of simulators to save computation time by saving and restoring the state of the system under simulation. However, even though such approaches aim to (bounded) formal verification, as a matter of fact, the simulator behaviour is not formally modelled and the proof of correctness of the proposed approaches basically relies on the intuitive notion of simulator behaviour. This gap makes it hard to check if the optimisations introduced to speed up the simulation do not actually omit checking relevant behaviours of the system under verification.
The aim of this paper is to fill the above gap by presenting a formal semantics for simulators.
△ Less
Submitted 23 September, 2015;
originally announced September 2015.
-
A Unifying Framework for Structural Properties of CSPs: Definitions, Complexity, Tractability
Authors:
Lucas Bordeaux,
Marco Cadoli,
Toni Mancini
Abstract:
Literature on Constraint Satisfaction exhibits the definition of several structural properties that can be possessed by CSPs, like (in)consistency, substitutability or interchangeability. Current tools for constraint solving typically detect such properties efficiently by means of incomplete yet effective algorithms, and use them to reduce the search space and boost search.
In this paper, we pro…
▽ More
Literature on Constraint Satisfaction exhibits the definition of several structural properties that can be possessed by CSPs, like (in)consistency, substitutability or interchangeability. Current tools for constraint solving typically detect such properties efficiently by means of incomplete yet effective algorithms, and use them to reduce the search space and boost search.
In this paper, we provide a unifying framework encompassing most of the properties known so far, both in CSP and other fields literature, and shed light on the semantical relationships among them. This gives a unified and comprehensive view of the topic, allows new, unknown, properties to emerge, and clarifies the computational complexity of the various detection problems.
In particular, among the others, two new concepts, fixability and removability emerge, that come out to be the ideal characterisations of values that may be safely assigned or removed from a variables domain, while preserving problem satisfiability. These two notions subsume a large number of known properties, including inconsistency, substitutability and others.
Because of the computational intractability of all the property-detection problems, by following the CSP approach we then determine a number of relaxations which provide sufficient conditions for their tractability. In particular, we exploit forms of language restrictions and local reasoning.
△ Less
Submitted 14 January, 2014;
originally announced January 2014.
-
Generalizing Consistency and other Constraint Properties to Quantified Constraints
Authors:
Lucas Bordeaux,
Marco Cadoli,
Toni Mancini
Abstract:
Quantified constraints and Quantified Boolean Formulae are typically much more difficult to reason with than classical constraints, because quantifier alternation makes the usual notion of solution inappropriate. As a consequence, basic properties of Constraint Satisfaction Problems (CSP), such as consistency or substitutability, are not completely understood in the quantified case. These proper…
▽ More
Quantified constraints and Quantified Boolean Formulae are typically much more difficult to reason with than classical constraints, because quantifier alternation makes the usual notion of solution inappropriate. As a consequence, basic properties of Constraint Satisfaction Problems (CSP), such as consistency or substitutability, are not completely understood in the quantified case. These properties are important because they are the basis of most of the reasoning methods used to solve classical (existentially quantified) constraints, and one would like to benefit from similar reasoning methods in the resolution of quantified constraints. In this paper, we show that most of the properties that are used by solvers for CSP can be generalized to quantified CSP. This requires a re-thinking of a number of basic concepts; in particular, we propose a notion of outcome that generalizes the classical notion of solution and on which all definitions are based. We propose a systematic study of the relations which hold between these properties, as well as complexity results regarding the decision of these properties. Finally, and since these problems are typically intractable, we generalize the approach used in CSP and propose weaker, easier to check notions based on locality, which allow to detect these properties incompletely but in polynomial time.
△ Less
Submitted 24 May, 2007;
originally announced May 2007.
-
Combining Relational Algebra, SQL, Constraint Modelling, and Local Search
Authors:
Marco Cadoli,
Toni Mancini
Abstract:
The goal of this paper is to provide a strong integration between constraint modelling and relational DBMSs. To this end we propose extensions of standard query languages such as relational algebra and SQL, by adding constraint modelling capabilities to them. In particular, we propose non-deterministic extensions of both languages, which are specially suited for combinatorial problems. Non-deter…
▽ More
The goal of this paper is to provide a strong integration between constraint modelling and relational DBMSs. To this end we propose extensions of standard query languages such as relational algebra and SQL, by adding constraint modelling capabilities to them. In particular, we propose non-deterministic extensions of both languages, which are specially suited for combinatorial problems. Non-determinism is introduced by means of a guessing operator, which declares a set of relations to have an arbitrary extension. This new operator results in languages with higher expressive power, able to express all problems in the complexity class NP. Some syntactical restrictions which make data complexity polynomial are shown. The effectiveness of both extensions is demonstrated by means of several examples. The current implementation, written in Java using local search techniques, is described. To appear in Theory and Practice of Logic Programming (TPLP)
△ Less
Submitted 11 January, 2006;
originally announced January 2006.
