| Records |
| 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 |
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 |
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 |
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 |
Toni Mancini; Enrico Tronci; Ivano Salvo; Federico Mari; Annalisa Massini; Igor Melatti |
| Title |
Computing Biological Model Parameters by Parallel Statistical Model Checking |
Type |
Journal Article |
| Year |
2015 |
Publication |
International Work Conference on Bioinformatics and Biomedical Engineering (IWBBIO 2015) |
Abbreviated Journal |
|
| Volume |
9044 |
Issue |
|
Pages |
542-554 |
| 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 |
124 |
| Permanent link to this record |
| |
|
| |
| 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 |
Tronci, E.; Mancini, T.; Salvo, I.; Mari, F.; Melatti, I.; Massini, A.; Sinisi, S.; Davì, F.; Dierkes, T.; Ehrig, R.; Röblitz, S.; Leeners, B.; Krüger, T.; Egli, M.; Ille, F. |
| Title |
Patient-Specific Models from Inter-Patient Biological Models and Clinical Records |
Type |
Conference Article |
| Year |
2014 |
Publication |
Formal Methods in Computer-Aided Design (FMCAD) |
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 |
120 |
| 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 |
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 |
Cavaliere, Federico; Mari, Federico; Melatti, Igor; Minei, Giovanni; Salvo, Ivano; Tronci, Enrico; Verzino, Giovanni; Yushtein, Yuri |
| Title |
Model Checking Satellite Operational Procedures |
Type |
Conference Article |
| Year |
2011 |
Publication |
DAta Systems In Aerospace (DASIA), Org. EuroSpace, Canadian Space Agency, CNES, ESA, EUMETSAT. San Anton, Malta, EuroSpace. |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
|
| Keywords |
|
| Abstract |
We present a model checking approach for the automatic verification of satellite operational procedures (OPs). Building a model for a complex system as a satellite is a hard task. We overcome this obstruction by using a suitable simulator (SIMSAT) for the satellite. Our approach aims at improving OP quality assurance by automatic exhaustive exploration of all possible simulation scenarios. Moreover, our solution decreases OP verification costs by using a model checker (CMurphi) to automatically drive the simulator. We model OPs as user-executed programs observing the simulator telemetries and sending telecommands to the simulator. In order to assess feasibility of our approach we present experimental results on a simple meaningful scenario. Our results show that we can save up to 90% of verification time. |
| 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 @ Dasia11 |
Serial |
13 |
| Permanent link to this record |
| |
|
| |
| Author |
Coppo, Mario; Dezani-Ciancaglini, Mariangiola; Giovannetti, Elio; Salvo, Ivano |
| Title |
Mobility Types for Mobile Processes in Mobile Ambients |
Type |
Journal Article |
| Year |
2003 |
Publication |
Electr. Notes Theor. Comput. Sci. |
Abbreviated Journal |
|
| Volume |
78 |
Issue |
|
Pages |
|
| Keywords |
|
| Abstract |
We present an ambient-like calculus in which the open capability is dropped, and a new form of “lightweight  process mobility is introduced. The calculus comes equipped with a type system that allows the kind of values exchanged in communications and the access and mobility properties of processes to be controlled. A type inference procedure determines the “minimal  requirements to accept a system or a component as well typed. This gives a kind of principal typing. As an expressiveness test, we show that some well known calculi of concurrency and mobility can be encoded in our calculus in a natural way. |
| 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 @ Coppo-Dezani-Giovannetti-Salvo:03 |
Serial |
74 |
| Permanent link to this record |
