| Records |
| Author |
Tronci, E.; Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Prodanovic, M.; Gruber, J. K.; Hayes, B.; Elmegaard, L. |
| Title |
Demand-Aware Price Policy Synthesis and Verification Services for Smart Grids |
Type  |
Conference Article |
| Year |
2014 |
Publication |
Proceedings of Smart Grid Communications (SmartGridComm), 2014 IEEE International Conference On |
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 @ melatti @ |
Serial |
121 |
| Permanent link to this record |
| |
|
| |
| Author |
Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Tronci, Enrico |
| Title |
Anytime System Level Verification via Random Exhaustive Hardware In The Loop Simulation |
Type |
Conference Article |
| Year |
2014 |
Publication |
In Proceedings of 17th EuroMicro Conference on Digital System Design (DSD 2014) |
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 |
122 |
| Permanent link to this record |
| |
|
| |
| Author |
Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Tronci, Enrico |
| Title |
SyLVaaS: System Level Formal Verification as a Service |
Type |
Conference Article |
| Year |
2015 |
Publication |
Proceedings of the 23rd Euromicro International Conference on Parallel, Distributed and Network-based Processing (PDP 2015), special session on Formal Approaches to Parallel and Distributed Systems (4PAD) |
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 |
123 |
| Permanent link to this record |
| |
|
| |
| Author |
Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Tronci, Enrico |
| Title |
Simulator Semantics for System Level Formal Verification |
Type |
Conference Article |
| Year |
2015 |
Publication |
Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2015), |
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 |
125 |
| Permanent link to this record |
| |
|
| |
| Author |
Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Minichino, Michele; Ciancamerla, Ester; Parisse, Andrea; Tronci, Enrico; Venturini Zilli, Marisa |
| Title |
Automatic Verification of a Turbogas Control System with the Mur$\varphi$ Verifier |
Type |
Conference Article |
| Year |
2003 |
Publication |
Hybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3-5, 2003, Proceedings |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
141-155 |
| Keywords |
|
| Abstract |
Automatic analysis of Hybrid Systems poses formidable challenges both from a modeling as well as from a verification point of view. We present a case study on automatic verification of a Turbogas Control System (TCS) using an extended version of the Mur$\varphi$ verifier. TCS is the heart of ICARO, a 2MW Co-generative Electric Power Plant. For large hybrid systems, as TCS is, the modeling effort accounts for a significant part of the whole verification activity. In order to ease our modeling effort we extended the Mur$\varphi$ verifier by importing the C language long double type (finite precision real numbers) into it. We give experimental results on running our extended Mur$\varphi$ on our TCS model. For example using Mur$\varphi$ we were able to compute an admissible range of values for the variation speed of the user demand of electric power to the turbogas. |
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
Springer |
Place of Publication |
|
Editor |
Maler, O.; Pnueli, A. |
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
| Series Volume |
2623 |
Series Issue |
|
Edition |
|
| ISSN |
3-540-00913-2 |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
yes |
| Call Number |
Sapienza @ mari @ Dimmcptz03 |
Serial |
88 |
| Permanent link to this record |
| |
|
| |
| Author |
Mazzini, Silvia; Puri, Stefano; Mari, Federico; Melatti, Igor; Tronci, Enrico |
| Title |
Formal Verification at System Level |
Type |
Conference Article |
| Year |
2009 |
Publication |
In: DAta Systems In Aerospace (DASIA), Org. EuroSpace, Canadian Space Agency, CNES, ESA, EUMETSAT. Instanbul, Turkey, EuroSpace |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
|
| Keywords |
|
| Abstract |
System Level Analysis calls for a language comprehensible to experts with different background and yet precise enough to support meaningful analyses. SysML is emerging as an effective balance between such conflicting goals. In this paper we outline some the results obtained as for SysML based system level functional formal verification by an ESA/ESTEC study, with a collaboration among INTECS and La Sapienza University of Roma. The study focuses on SysML based system level functional requirements techniques. |
| 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 |
yes |
| Call Number |
Sapienza @ mari @ Dasia09 |
Serial |
20 |
| 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 |
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.; Melatti, I.; Salvo, I.; Tronci, E.; Gruber, J.K.; Hayes, B.; Prodanovic, M.; Elmegaard, L. |
| Title |
User Flexibility Aware Price Policy Synthesis for Smart Grids |
Type |
Conference Article |
| Year |
2015 |
Publication |
Digital System Design (DSD), 2015 Euromicro Conference on |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
478-485 |
| Keywords |
Contracts; Current measurement; Load management; Power demand; Power measurement; State estimation; Substations; Grid State Estimation; Peak Shaving; Policy Robustness Verification; Price Policy Synthesis |
| 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 @ preissler @ Mancini_etal2015_3 |
Serial |
136 |
| 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 |
| |
|
| |
| Author |
Ehrig, R.; Dierkes, T.; Schaefer, S.; Roeblitz, S.; Tronci, E.; Mancini, T.; Salvo, I.; Alimguzhin, V.; Mari, F.; Melatti, I.; Massini, A.; Leeners, B.; Krueger, T.H.C.; Egli, M.; Ille, F. |
| Title |
An integrative approach for model driven computation of treatments in reproductive medicine |
Type |
Conference Article |
| Year |
2015 |
Publication |
Proceedings of the 15th International Symposium on Mathematical and Computational Biology (BIOMAT 2015), Rorkee, India |
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 @ preissler @ Ehrig_etal2015 |
Serial |
144 |
| Permanent link to this record |
