|   | 
Details
   web
Records
Author Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Merli, Fabio; Tronci, Enrico
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 Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 8044 Series Issue (down) 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 Della Penna, Giuseppe; Intrigila, Benedetto; Magazzeni, Daniele; Melatti, Igor; Tronci, Enrico
Title CGMurphi: Automatic synthesis of numerical controllers for nonlinear hybrid systems Type Journal Article
Year 2013 Publication European Journal of Control Abbreviated Journal European Journal of Control
Volume 19 Issue 1 Pages 14-36
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Elsevier North-Holland, Inc. Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue (down) Edition
ISSN 0947-3580 ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number Sapienza @ melatti @ Serial 114
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 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 Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue (down) Edition
ISSN 1942-2628 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ melatti @ Serial 115
Permanent link to this record
 

 
Author Verzino Giovanni ; Cavaliere, Federico; Mari, Federico; Melatti, Igor; Minei, Giovanni; Salvo, Ivano; Yushtein, Yuri; Tronci, Enrico
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 Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue (down) Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number Sapienza @ melatti @ Serial 117
Permanent link to this record
 

 
Author Mancini, Toni ; Mari, Federico ; Massini, Annalisa; Melatti, Igor; Tronci, Enrico
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 Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue (down) Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number Sapienza @ melatti @ Serial 118
Permanent link to this record
 

 
Author Tronci, E.; Mancini, T.; Mari, F.; Melatti, I.; Jacobsen, R. H.; Ebeid, E.; Mikkelsen, S. A.; Prodanovic, M.; Gruber, J. K.; Hayes, B.
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 Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue (down) 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 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 (down) Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number Sapienza @ mari @ Serial 120
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 (down) 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 (down) 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 (down) Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number MCLab @ davi @ Serial 123
Permanent link to this record