| |
Records |
Links |
|
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 |
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.; 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 |
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.; Massini, A.; Melatti, I.; Tronci, E. |
|
| |
Title |
On Checking Equivalence of Simulation Scripts |
Type |
Journal Article |
| |
Year |
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 |
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 |
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 |
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 |
Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico; Alvisi, Lorenzo; Clement, Allen; Li, Harry |
|
| |
Title |
Model Checking Nash Equilibria in MAD Distributed Systems |
Type |
Conference Article |
| |
Year |
2008 |
Publication |
FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
1-8 |
|
| |
Keywords |
Model Checking, MAD Distributed System, Nash Equilibrium |
|
| |
Abstract |
We present a symbolic model checking algorithm for verification of Nash equilibria in finite state mechanisms modeling Multiple Administrative Domains (MAD) distributed systems. Given a finite state mechanism, a proposed protocol for each agent and an indifference threshold for rewards, our model checker returns PASS if the proposed protocol is a Nash equilibrium (up to the given indifference threshold) for the given mechanism, FAIL otherwise. We implemented our model checking algorithm inside the NuSMV model checker and present experimental results showing its effectiveness for moderate size mechanisms. For example, we can handle mechanisms which corresponding normal form games would have more than $10^20$ entries. To the best of our knowledge, no model checking algorithm for verification of mechanism Nash equilibria has been previously published. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
IEEE Press |
Place of Publication |
Piscataway, NJ, USA |
Editor |
Cimatti, A.; Jones, R. |
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
| |
Series Volume |
|
Series Issue |
|
Edition |
|
|
| |
ISSN |
978-1-4244-2735-2 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ MarMelSalTroAlvCle08 |
Serial |
93 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
|
| |
Title |
From Boolean Relations to Control Software |
Type |
Conference Article |
| |
Year |
2011 |
Publication |
Proceedings of ICSEA 2011, The Sixth International Conference on Software Engineering Advances |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
528-533 |
|
| |
Keywords |
|
|
| |
Abstract |
Many software as well digital hardware automatic synthesis methods define the set of implementations meeting the given system specifications with a boolean relation K. In such a context a fundamental step in the software (hardware) synthesis process is finding effective solutions to the functional equation defined by K. This entails finding a (set of) boolean function(s) F (typically represented using OBDDs, Ordered Binary Decision Diagrams) such that: 1) for all x for which K is satisfiable, K(x, F(x)) = 1 holds; 2) the implementation of F is efficient with respect to given implementation parameters such as code size or execution time. While this problem has been widely studied in digital hardware synthesis, little has been done in a software synthesis context. Unfortunately the approaches developed for hardware synthesis cannot be directly used in a software context. This motivates investigation of effective methods to solve the above problem when F has to be implemented with software. In this paper we present an algorithm that, from an OBDD representation for K, generates a C code implementation for F that has the same size as the OBDD for F and a WCET (Worst Case Execution Time) linear in nr, being n = |x| the number of input arguments for functions in F and r the number of functions in F. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
ThinkMind |
Place of Publication |
|
Editor |
|
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
| |
Series Volume |
|
Series Issue |
|
Edition |
|
|
| |
ISSN |
978-1-61208-165-6 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
Best Paper Award |
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ icsea11 |
Serial |
14 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
|
| |
Title |
Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems |
Type |
Conference Article |
| |
Year |
2010 |
Publication |
Computer Aided Verification |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
180-195 |
|
| |
Keywords |
|
|
| |
Abstract |
We present an algorithm that given a Discrete Time Linear Hybrid System returns a correct-by-construction software implementation K for a (near time optimal) robust quantized feedback controller for along with the set of states on which K is guaranteed to work correctly (controllable region). Furthermore, K has a Worst Case Execution Time linear in the number of bits of the quantization schema. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
Springer Berlin / Heidelberg |
Place of Publication |
|
Editor |
Touili, T.; Cook, B.; Jackson, P. |
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
|
| |
Series Volume |
6174 |
Series Issue |
|
Edition |
|
|
| |
ISSN |
|
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ cav2010 |
Serial |
16 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Bobbio, Andrea; Ciancamerla, Ester; Di Blasi, Saverio; Iacomini, Alessandro; Mari, Federico; Melatti, Igor; Minichino, Michele; Scarlatti, Alessandro; Tronci, Enrico; Terruggia, Roberta; Zendri, Emilio |
|
| |
Title |
Risk analysis via heterogeneous models of SCADA interconnecting Power Grids and Telco networks |
Type |
Conference Article |
| |
Year |
2009 |
Publication |
Proceedings of Fourth International Conference on Risks and Security of Internet and Systems (CRiSIS) |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
90-97 |
|
| |
Keywords |
|
|
| |
Abstract |
The automation of power grids by means of supervisory control and data acquisition (SCADA) systems has led to an improvement of power grid operations and functionalities but also to pervasive cyber interdependencies between power grids and telecommunication networks. Many power grid services are increasingly depending upon the adequate functionality of SCADA system which in turn strictly depends on the adequate functionality of its communication infrastructure. We propose to tackle the SCADA risk analysis by means of different and heterogeneous modeling techniques and software tools. We demonstrate the applicability of our approach through a case study on an actual SCADA system for an electrical power distribution grid. The modeling techniques we discuss aim at providing a probabilistic dependability analysis, followed by a worst case analysis in presence of malicious attacks and a real-time performance evaluation. |
|
| |
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 |
Fourth International Conference on Risks and Security of Internet and Systems (CRiSIS) |
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ crisis09 |
Serial |
17 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico; Alvisi, Lorenzo; Clement, Allen; Li, Harry |
|
| |
Title |
Model Checking Coalition Nash Equilibria in MAD Distributed Systems |
Type |
Conference Article |
| |
Year |
2009 |
Publication |
Stabilization, Safety, and Security of Distributed Systems, 11th International Symposium, SSS 2009, Lyon, France, November 3-6, 2009. Proceedings |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
531-546 |
|
| |
Keywords |
|
|
| |
Abstract |
We present two OBDD based model checking algorithms for the verification of Nash equilibria in finite state mechanisms modeling Multiple Administrative Domains (MAD) distributed systems with possibly colluding agents (coalitions) and with possibly faulty or malicious nodes (Byzantine agents). Given a finite state mechanism, a proposed protocol for each agent and the maximum sizes f for Byzantine agents and q for agents collusions, our model checkers return Pass if the proposed protocol is an ε-f-q-Nash equilibrium, i.e. no coalition of size up to q may have an interest greater than ε in deviating from the proposed protocol when up to f Byzantine agents are present, Fail otherwise. We implemented our model checking algorithms within the NuSMV model checker: the first one explicitly checks equilibria for each coalition, while the second represents symbolically all coalitions. We present experimental results showing their effectiveness for moderate size mechanisms. For example, we can verify coalition Nash equilibria for mechanisms which corresponding normal form games would have more than $5 \times 10^21$ entries. Moreover, we compare the two approaches, and the explicit algorithm turns out to outperform the symbolic one. To the best of our knowledge, no model checking algorithm for verification of Nash equilibria of mechanisms with coalitions has been previously published. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
Springer |
Place of Publication |
|
Editor |
Guerraoui, R.; Petit, F. |
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
|
| |
Series Volume |
5873 |
Series Issue |
|
Edition |
|
|
| |
ISSN |
|
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ sss09 |
Serial |
19 |
|
| Permanent link to this record |
