|   | 
Details
   web
Records
Author Melatti, I.; Mari, F.; Mancini, T.; Prodanovic, M.; Tronci, E.
Title A Two-Layer Near-Optimal Strategy for Substation Constraint Management via Home Batteries Type Journal Article
Year (down) 2021 Publication IEEE Transactions on Industrial Electronics Abbreviated Journal
Volume Issue Pages 1-1
Keywords
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 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.
Address
Corporate Author Thesis
Publisher Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN ISBN Medium
Area Expedition Conference
Notes To appear Approved no
Call Number MCLab @ davi @ ref9513535 Serial 190
Permanent link to this record
 

 
Author Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E.
Title On Checking Equivalence of Simulation Scripts Type Journal Article
Year (down) 2021 Publication Journal of Logical and Algebraic Methods in Programming Abbreviated Journal
Volume Issue Pages 100640
Keywords Formal verification, Simulation based formal verification, Formal Verification of cyber-physical systems, System-level formal verification
Abstract To support Model Based Design of Cyber-Physical Systems (CPSs) many simulation based approaches to System Level Formal Verification (SLFV) have been devised. Basically, these are Bounded Model Checking approaches (since simulation horizon is of course bounded) relying on simulators to compute the system dynamics and thereby verify the given system properties. The main obstacle to simulation based SLFV is the large number of simulation scenarios to be considered and thus the huge amount of simulation time needed to complete the verification task. To save on computation time, simulation based SLFV approaches exploit the capability of simulators to save and restore simulation states. Essentially, such a time saving is obtained by optimising the simulation script defining the simulation activity needed to carry out the verification task. Although such approaches aim to (bounded) formal verification, as a matter of fact, the proof of correctness of the methods to optimise simulation scripts basically relies on an intuitive semantics for simulation scripting languages. This hampers the possibility of formally showing that the optimisations introduced to speed up the simulation activity do not actually omit checking of relevant behaviours for the system under verification. The aim of this paper is to fill the above gap by presenting an operational semantics for simulation scripting languages and by proving soundness and completeness properties for it. This, in turn, enables formal proofs of equivalence between unoptimised and optimised simulation scripts.
Address
Corporate Author Thesis
Publisher Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 2352-2208 ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number MCLab @ davi @ Mancini2021100640 Serial 183
Permanent link to this record
 

 
Author Sinisi, S.; Alimguzhin, V.; Mancini, T.; Tronci, E.; Mari, F.; Leeners, B.
Title Optimal Personalised Treatment Computation through In Silico Clinical Trials on Patient Digital Twins Type Journal Article
Year (down) 2020 Publication Abbreviated Journal Fundamenta Informaticae
Volume 174 Issue Pages 283-310
Keywords Artificial Intelligence; Virtual Physiological Human; In Silico Clinical Trials; Simulation; Personalised Medicine; In Silico Treatment Optimisation
Abstract In Silico Clinical Trials (ISCT), 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 (ISCT) guided by intelligent search, optimise a pharmacological treatment for an individual patient (precision medicine ). We 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.
Address
Corporate Author Thesis
Publisher IOS Press Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 1875-8681 ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number MCLab @ davi @ Serial 187
Permanent link to this record
 

 
Author Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Salvo, I.; Sinisi, S.; Tronci, E.; Ehrig, R.; Röblitz, S.; Leeners, B.
Title Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction Type Conference Article
Year (down) 2018 Publication 25th RCRA International Workshop on “Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion” (RCRA 2018) Abbreviated Journal
Volume Issue Pages
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number MCLab @ davi @ Serial 175
Permanent link to this record
 

 
Author Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E.; Gruber, J.; Hayes, B.; Prodanovic, M.; Elmegaard, L.
Title Parallel Statistical Model Checking for Safety Verification in Smart Grids Type Conference Article
Year (down) 2018 Publication 2018 IEEE International Conference on Communications, Control, and Computing Technologies for Smart Grids (SmartGridComm) Abbreviated Journal
Volume Issue Pages 1-6
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number MCLab @ davi @ mancini-etal:2018:smartgridcomm Serial 170
Permanent link to this record
 

 
Author Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E.
Title An Efficient Algorithm for Network Vulnerability Analysis Under Malicious Attacks Type Conference Article
Year (down) 2018 Publication Foundations of Intelligent Systems – 24th International Symposium, ISMIS 2018, Limassol, Cyprus, October 29-31, 2018, Proceedings Abbreviated Journal
Volume Issue Pages 302-312
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Best Paper Approved no
Call Number MCLab @ davi @ DBLP:conf/ismis/ManciniMMST18 Serial 176
Permanent link to this record
 

 
Author Mancini, T. ; Mari, F.; Massini, A.; Melatti, I.; Salvo, I.; Tronci, E.
Title On minimising the maximum expected verification time Type Journal Article
Year (down) 2017 Publication Information Processing Letters Abbreviated Journal
Volume Issue Pages
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number Sapienza @ mari @ Serial 163
Permanent link to this record
 

 
Author Alimguzhin, V.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E.
Title Linearising Discrete Time Hybrid Systems Type Journal Article
Year (down) 2017 Publication IEEE Transactions on Automatic Control Abbreviated Journal
Volume 62 Issue 10 Pages 5357-5364
Keywords
Abstract Model Based Design approaches for embedded systems aim at generating correct-by-construction control software, guaranteeing that the closed loop system (controller and plant) meets given system level formal specifications. This technical note addresses control synthesis for safety and reachability properties of possibly non-linear discrete time hybrid systems. By means of syntactical transformations that require non-linear terms to be Lipschitz continuous functions, we over-approximate non-linear dynamics with a linear system whose controllers are guaranteed to be controllers of the original system. We evaluate performance of our approach on meaningful control synthesis benchmarks, also comparing it to a state-of-the-art tool.
Address
Corporate Author Thesis
Publisher Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 0018-9286 ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number Sapienza @ mari @ ref7902199 Serial 164
Permanent link to this record
 

 
Author Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E.
Title SyLVaaS: System Level Formal Verification as a Service Type Journal Article
Year (down) 2016 Publication Fundamenta Informaticae Abbreviated Journal
Volume 149 Issue 1-2 Pages 101-132
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number MCLab @ davi @ DBLP:journals/fuin/ManciniMMMT16 Serial 160
Permanent link to this record
 

 
Author Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E.
Title Anytime system level verification via parallel random exhaustive hardware in the loop simulation Type Journal Article
Year (down) 2016 Publication Microprocessors and Microsystems Abbreviated Journal
Volume 41 Issue Pages 12-28
Keywords Model Checking of Hybrid Systems; Model checking driven simulation; Hardware in the loop simulation
Abstract Abstract System level verification of cyber-physical systems has the goal of verifying that the whole (i.e., software + hardware) system meets the given specifications. Model checkers for hybrid systems cannot handle system level verification of actual systems. Thus, Hardware In the Loop Simulation (HILS) is currently the main workhorse for system level verification. By using model checking driven exhaustive HILS, System Level Formal Verification (SLFV) can be effectively carried out for actual systems. We present a parallel random exhaustive HILS based model checker for hybrid systems that, by simulating all operational scenarios exactly once in a uniform random order, is able to provide, at any time during the verification process, an upper bound to the probability that the System Under Verification exhibits an error in a yet-to-be-simulated scenario (Omission Probability). We show effectiveness of the proposed approach by presenting experimental results on SLFV of the Inverted Pendulum on a Cart and the Fuel Control System examples in the Simulink distribution. To the best of our knowledge, no previously published model checker can exhaustively verify hybrid systems of such a size and provide at any time an upper bound to the Omission Probability.
Address
Corporate Author Thesis
Publisher Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 0141-9331 ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number MCLab @ davi @ Mancini201612 Serial 155
Permanent link to this record