| Records |
| Author |
Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E. |
| Title |
SyLVaaS: System Level Formal Verification as a Service |
Type |
|
| Year |
2016 |
Publication |
Fundam. Inform. |
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 |
|
| Call Number |
UNIROMA1 @ davi @ DBLP:journals/fuin/ManciniMMMT16 |
Serial |
63 |
| Permanent link to this record |
| |
|
| |
| Author |
Mancini, T. |
| Title |
Now or Never: Negotiating Efficiently with Unknown or Untrusted Counterparts |
Type |
|
| Year |
2016 |
Publication |
Fundam. Inform. |
Abbreviated Journal |
|
| Volume |
149 |
Issue |
1-2 |
Pages |
61-100 |
| 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 |
|
| Call Number |
UNIROMA1 @ davi @ DBLP:journals/fuin/Mancini16 |
Serial |
62 |
| Permanent link to this record |
| |
|
| |
| Author |
Jacobsen, R.H.; Mikkelsen, S.A. |
| Title |
Infrastructure for Intelligent Automation Services in the Smart Grid |
Type |
|
| Year |
2014 |
Publication |
Wireless Personal Communications |
Abbreviated Journal |
|
| Volume |
76 |
Issue |
2 |
Pages |
125-147 |
| Keywords |
Home area network; Smart energy profile; Intelligent automation services; Smart grid |
| Abstract |
|
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
Springer US |
Place of Publication |
|
Editor |
|
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
| Series Volume |
|
Series Issue |
|
Edition |
|
| ISSN |
0929-6212 |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
|
| Call Number |
UNIROMA1 @ davi @ JacMik14 |
Serial |
41 |
| 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 |
|
| Year |
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 |
|
| Call Number |
UNIROMA1 @ davi @ Mancini201612 |
Serial |
59 |
| Permanent link to this record |
| |
|
| |
| Author |
Mari, F.; Melatti, I.; Salvo, I.; Tronci, E. |
| Title |
Model Based Synthesis of Control Software from System Level Formal Specifications |
Type |
|
| Year |
2014 |
Publication |
Acm Transactions On Software Engineering And Methodology |
Abbreviated Journal |
|
| Volume |
23 |
Issue |
1 |
Pages |
6 |
| Keywords |
|
| Abstract |
|
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
Acm |
Place of Publication |
|
Editor |
|
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
| Series Volume |
|
Series Issue |
|
Edition |
|
| ISSN |
1049-331x |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
|
| Call Number |
UNIROMA1 @ davi @ Mari_etal2014 |
Serial |
40 |
| Permanent link to this record |
| |
|
| |
| Author |
Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
| Title |
Linear Constraints and Guarded Predicates as a Modeling Language for Discrete Time Hybrid Systems |
Type |
|
| Year |
2013 |
Publication |
International Journal on Advances in Software |
Abbreviated Journal |
|
| Volume |
vol. 6, nr 1&2 |
Issue |
|
Pages |
155-169 |
| Keywords |
Model-based software design; Linear predicates; Hybrid systems |
| Abstract |
Model based design is particularly appealing insoftware based control systems (e.g., embeddedsoftware) design, since in such a case systemlevel specifications are much easier to definethan the control software behavior itself. Inturn, model based design of embedded systemsrequires modeling both continuous subsystems(typically, the plant) as well as discretesubsystems (the controller). This is typicallydone using hybrid systems. Mixed Integer LinearProgramming (MILP) based abstraction techniqueshave been successfully applied to automatically synthesize correct-by-construction controlsoftware for discrete time linear hybrid systems,where plant dynamics is modeled as a linearpredicate over state, input, and next statevariables. Unfortunately, MILP solvers requiresuch linear predicates to be conjunctions oflinear constraints, which is not a natural way ofmodeling hybrid systems. In this paper we showthat, under the hypothesis that each variableranges over a bounded interval, any linearpredicate built upon conjunction and disjunction of linear constraints can be automaticallytranslated into an equivalent conjunctivepredicate. Since variable bounds play a key rolein this translation, our algorithm includes aprocedure to compute all implicit variable boundsof the given linear predicate. Furthermore, weshow that a particular form of linear predicates,namely guarded predicates, are a natural andpowerful language to succinctly model discretetime linear hybrid systems dynamics. Finally, weexperimentally show the feasibility of ourapproach on an important and challenging casestudy taken from the literature, namely themulti-input Buck DC-DC Converter. As an example,the guarded predicate that models (with 57constraints) a 6-inputs Buck DC-DC Converter istranslated in a conjunctive predicate (with 102linear constraints) in about 40 minutes. |
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
Iaria |
Place of Publication |
|
Editor |
|
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
| Series Volume |
|
Series Issue |
|
Edition |
|
| ISSN |
1942-2628 |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
|
| Call Number |
UNIROMA1 @ davi @ Mari_etal2013 |
Serial |
22 |
| Permanent link to this record |
| |
|
| |
| Author |
Mikkelsen, S.A.; Jacobsen, R.H. |
| Title |
Consumer-Centric and Service-Oriented Architecture for the Envisioned Energy Internet |
Type |
|
| Year |
2015 |
Publication |
Digital System Design (DSD), 2015 Euromicro Conference on |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
301-305 |
| Keywords |
Authorization;Computer architecture;Data privacy;Home appliances;Privacy;Protocols;Smart grids;data privacy;smart grid;web services |
| 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 |
|
| Call Number |
UNIROMA1 @ davi @ ref7302289 |
Serial |
56 |
| Permanent link to this record |
| |
|
| |
| Author |
Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
| Title |
On Model Based Synthesis of Embedded Control Software |
Type |
|
| Year |
2012 |
Publication |
International Conference on Embedded Software, EMSOFT |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
|
| Keywords |
|
| Abstract |
|
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
ACM |
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 |
|
| Call Number |
UNIROMA1 @ mari @ Alimguzhin_etal2012_2 |
Serial |
14 |
| Permanent link to this record |
| |
|
| |
| Author |
Hayes, B. P.; Prodanovic, M. |
| Title |
A comparison of MV distribution system state estimation methods using field data |
Type |
|
| Year |
2015 |
Publication |
IEEE PES General Meeting, Denver, CO, United States |
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 |
|
| Call Number |
UNIROMA1 @ davi @ |
Serial |
52 |
| Permanent link to this record |
| |
|
| |
| Author |
Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E. |
| Title |
Simulator Semantics for System Level Formal Verification |
Type |
|
| 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 |
|
| Call Number |
UNIROMA1 @ davi @ |
Serial |
54 |
| Permanent link to this record |
