| |
Records |
Links |
|
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 |
Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
|
| |
Title |
On-the-Fly Control Software Synthesis |
Type |
|
| |
Year |
2013 |
Publication |
Proc. of International SPIN Symposium on Model Checking of Software (SPIN 2013) |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
61-80 |
|
| |
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 |
7976 |
Series Issue |
|
Edition |
|
|
| |
ISSN |
978-3-642-39175-0 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
|
|
| |
Call Number |
UNIROMA1 @ davi @ Alimguzhin_etal2013 |
Serial |
18 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
|
| |
Title |
A Map-Reduce Parallel Approach to Automatic Synthesis of Control Software |
Type |
|
| |
Year |
2013 |
Publication |
Proc. of International SPIN Symposium on Model Checking of Software (SPIN 2013) |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
43-60 |
|
| |
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 |
7976 |
Series Issue |
|
Edition |
|
|
| |
ISSN |
978-3-642-39175-0 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
|
|
| |
Call Number |
UNIROMA1 @ davi @ Alimguzhin_etal2013_2 |
Serial |
19 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Merli, Fabio; Tronci, Enrico |
|
| |
Title |
System Level Formal Verification via Model Checking Driven Simulation |
Type |
|
| |
Year |
2013 |
Publication |
Proceedings of the 25th International Conference on Computer Aided Verification (CAV 2013). July 13–19, 2013, Saint Petersburg, Russia |
Abbreviated Journal |
|
|
| |
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 |
|
Edition |
|
|
| |
ISSN |
978-3-642-39798-1 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
|
|
| |
Call Number |
UNIROMA1 @ davi @ Mancini_etal2013 |
Serial |
21 |
|
| 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 |
Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E. |
|
| |
Title |
System Level Formal Verification via Distributed Multi-Core Hardware in the Loop Simulation |
Type |
|
| |
Year |
2014 |
Publication |
Proc. of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Computing (PDP 2014) |
Abbreviated Journal |
|
|
| |
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 |
|
Edition |
|
|
| |
ISSN |
|
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
|
|
| |
Call Number |
UNIROMA1 @ davi @ Mancini_etal2014 |
Serial |
39 |
|
| 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 |
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 |
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 |
|
| |
Year |
2014 |
Publication |
Proceedings of the Work in Progress Session of DSD/SEAA 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 |
978-3-902457-40-0 |
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
|
|
| |
Call Number |
UNIROMA1 @ davi @ |
Serial |
42 |
|
| 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 |
|
| |
Year |
2014 |
Publication |
Proceedings of the 5th IEEE International Conference On Smart Grid Communications (SmartGridComm 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 |
|
|
| |
Call Number |
UNIROMA1 @ davi @ Tronci_etal2014 |
Serial |
43 |
|
| Permanent link to this record |
