toggle visibility Search & Display Options

Select All    Deselect All
 |   | 
Details
   print
  Records Links
Author Tronci, E.; Mancini, T.; Mari, F.; Melatti, I.; Jacobsen, R. H.; Ebeid, E.; Mikkelsen, S. A.; Prodanovic, M.; Gruber, J. K.; Hayes, B. pdf  isbn
openurl 
  Title SmartHG: Energy Demand Aware Open Services for Smart Grid Intelligent Automation Type Conference Article
  Year 2014 Publication Proceedings of the Work in Progress Session of SEAA/DSD 2014 Abbreviated Journal  
  Volume Issue Pages  
  Keywords  
  Abstract  
  Address  
  Corporate Author Thesis  
  Publisher Place of Publication Editor  
  Language (up) Summary Language Original Title  
  Series Editor Series Title Abbreviated Series Title  
  Series Volume Series Issue Edition  
  ISSN ISBN 978-3-902457-40-0 Medium  
  Area Expedition Conference  
  Notes Approved no  
  Call Number Sapienza @ mari @ Serial 119  
Permanent link to this record
 

 
Author Mancini, Toni ; Mari, Federico ; Massini, Annalisa; Melatti, Igor; Tronci, Enrico pdf  doi
openurl 
  Title System Level Formal Verification via Distributed Multi-Core Hardware in the Loop Simulation Type Conference Article
  Year 2014 Publication Proc. of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing Abbreviated Journal Euromicro International Conference on Parallel, Distributed and Network-Based Processing  
  Volume Issue Pages  
  Keywords  
  Abstract  
  Address  
  Corporate Author Thesis  
  Publisher IEEE Computer Society Place of Publication Editor  
  Language (up) 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 118  
Permanent link to this record
 

 
Author Verzino Giovanni ; Cavaliere, Federico; Mari, Federico; Melatti, Igor; Minei, Giovanni; Salvo, Ivano; Yushtein, Yuri; Tronci, Enrico pdf  doi
openurl 
  Title Model checking driven simulation of sat procedures Type Conference Article
  Year 2012 Publication Proceedings of 12th International Conference on Space Operations (SpaceOps 2012) Abbreviated Journal International Conference on Space Operations  
  Volume Issue Pages  
  Keywords  
  Abstract  
  Address  
  Corporate Author Thesis  
  Publisher Place of Publication Editor  
  Language (up) 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 117  
Permanent link to this record
 

 
Author Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico pdf  url
openurl 
  Title Linear Constraints and Guarded Predicates as a Modeling Language for Discrete Time Hybrid Systems Type Journal Article
  Year 2013 Publication International Journal on Advances in Software Abbreviated Journal Intern. Journal on Advances in SW  
  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 in
software based control systems (e.g., embedded
software) design, since in such a case system
level specifications are much easier to define
than the control software behavior itself. In
turn, model based design of embedded systems
requires modeling both continuous subsystems
(typically, the plant) as well as discrete
subsystems (the controller). This is typically
done using hybrid systems. Mixed Integer Linear
Programming (MILP) based abstraction techniques
have been successfully applied to automatically
synthesize correct-by-construction control
software for discrete time linear hybrid systems,
where plant dynamics is modeled as a linear
predicate over state, input, and next state
variables. Unfortunately, MILP solvers require
such linear predicates to be conjunctions of
linear constraints, which is not a natural way of
modeling hybrid systems. In this paper we show
that, under the hypothesis that each variable
ranges over a bounded interval, any linear
predicate built upon conjunction and disjunction
of linear constraints can be automatically
translated into an equivalent conjunctive
predicate. Since variable bounds play a key role
in this translation, our algorithm includes a
procedure to compute all implicit variable bounds
of the given linear predicate. Furthermore, we
show that a particular form of linear predicates,
namely guarded predicates, are a natural and
powerful language to succinctly model discrete
time linear hybrid systems dynamics. Finally, we
experimentally show the feasibility of our
approach on an important and challenging case
study taken from the literature, namely the
multi-input Buck DC-DC Converter. As an example,
the guarded predicate that models (with 57
constraints) a 6-inputs Buck DC-DC Converter is
translated in a conjunctive predicate (with 102
linear constraints) in about 40 minutes.
 
  Address  
  Corporate Author Thesis  
  Publisher IARIA Place of Publication Editor Luigi Lavazza  
  Language (up) 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 yes  
  Call Number Sapienza @ melatti @ Serial 115  
Permanent link to this record
 

 
Author Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Merli, Fabio; Tronci, Enrico pdf  doi
isbn  openurl
  Title System Level Formal Verification via Model Checking Driven Simulation Type Conference Article
  Year 2013 Publication Proceedings of the 25th International Conference on Computer Aided Verification. July 13-19, 2013, Saint Petersburg, Russia Abbreviated Journal CAV 2013  
  Volume Issue Pages 296-312  
  Keywords  
  Abstract  
  Address  
  Corporate Author Thesis  
  Publisher Springer - Verlag Place of Publication Editor  
  Language (up) Summary Language Original Title  
  Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title  
  Series Volume 8044 Series Issue Edition  
  ISSN 0302-9743 ISBN 978-3-642-39798-1 Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ Serial 113  
Permanent link to this record
 

 
Author Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico url  openurl
  Title Automatic Control Software Synthesis for Quantized Discrete Time Hybrid Systems Type Report
  Year 2012 Publication Abbreviated Journal  
  Volume abs/1207.4098 Issue Pages  
  Keywords  
  Abstract Many Embedded Systems are indeed Software Based Control Systems, that is control systems whose controller consists of control software running on a microcontroller device. This motivates investigation on Formal Model Based Design approaches for automatic synthesis of embedded systems control software. This paper addresses control software synthesis for discrete time nonlinear systems. We present a methodology to overapproximate the dynamics of a discrete time nonlinear hybrid system H by means of a discrete time linear hybrid system L(H), in such a way that controllers for L(H) are guaranteed to be controllers for H. We present experimental results on the inverted pendulum, a challenging and meaningful benchmark in nonlinear Hybrid Systems control.  
  Address  
  Corporate Author Thesis  
  Publisher CoRR, Technical Report Place of Publication Editor  
  Language (up) 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 @ Serial 103  
Permanent link to this record
 

 
Author Alimguzhin, V.; Mari, F.; Melatti, I.; Tronci, E.; Ebeid, E.; Mikkelsen, S.A.; Jacobsen, R.H.; Gruber, J.K.; Hayes, B.; Huerta, F.; Prodanovic, M. pdf  doi
openurl 
  Title A Glimpse of SmartHG Project Test-bed and Communication Infrastructure Type Conference Article
  Year 2015 Publication Digital System Design (DSD), 2015 Euromicro Conference on Abbreviated Journal  
  Volume Issue Pages 225-232  
  Keywords Batteries; Control systems; Databases; Production; Sensors; Servers; Smart grids; Grid State Estimation; Peak Shaving; Policy Robustness Verification; Price Policy Synthesis  
  Abstract  
  Address  
  Corporate Author Thesis  
  Publisher Place of Publication Editor  
  Language (up) 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 @ Alimguzhin_etal2015 Serial 127  
Permanent link to this record
 

 
Author Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E. pdf  url
doi  openurl
  Title Anytime system level verification via parallel random exhaustive hardware in the loop simulation Type Journal Article
  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 (up) 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
 

 
Author Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E. pdf  url
doi  openurl
  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 (up) 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. pdf  doi
openurl 
  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 (up) 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
Select All    Deselect All
 |   | 
Details
   print

Save Citations:
Export Records: