|   | 
Details
   web
Records
Author Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title Automatic Control Software Synthesis for Quantized Discrete Time Hybrid Systems Type Report
Year 2012 Publication Abbreviated Journal
Volume abs/1207.4098 Issue (up) 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 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, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title A Map-Reduce Parallel Approach to Automatic Synthesis of Control Software Type Report
Year 2012 Publication Abbreviated Journal
Volume abs/1210.2276 Issue (up) Pages
Keywords
Abstract Many Control Systems are indeed Software Based Control Systems, i.e. 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 control software.
Available algorithms and tools (e.g., QKS) may require weeks or even months of computation to synthesize control software for large-size systems. This motivates search for parallel algorithms for control software synthesis.
In this paper, we present a map-reduce style parallel algorithm for control software synthesis when the controlled system (plant) is modeled as discrete time linear hybrid system. Furthermore we present an MPI-based implementation PQKS of our algorithm. To the best of our knowledge, this is the first parallel approach for control software synthesis.
We experimentally show effectiveness of PQKS on two classical control synthesis problems: the inverted pendulum and the multi-input buck DC/DC converter. Experiments show that PQKS efficiency is above 65%. As an example, PQKS requires about 16 hours to complete the synthesis of control software for the pendulum on a cluster with 60 processors, instead of the 25 days needed by the sequential algorithm in QKS.
Address
Corporate Author Thesis
Publisher CoRR, Technical Report 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 @ Serial 101
Permanent link to this record
 

 
Author Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title Control Software Visualization Type Conference Article
Year 2012 Publication Proceedings of INFOCOMP 2012, The Second International Conference on Advanced Communications and Computation Abbreviated Journal
Volume Issue (up) Pages 15-20
Keywords
Abstract
Address
Corporate Author Thesis
Publisher ThinkMind Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 978-1-61208-226-4 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ infocomp2012 Serial 100
Permanent link to this record
 

 
Author Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title Undecidability of Quantized State Feedback Control for Discrete Time Linear Hybrid Systems Type Book Chapter
Year 2012 Publication Theoretical Aspects of Computing – ICTAC 2012 Abbreviated Journal
Volume Issue (up) Pages 243-258
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Springer Berlin Heidelberg Place of Publication Editor Roychoudhury, A.; D'Souza, M.
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 7521 Series Issue Edition
ISSN ISBN 978-3-642-32942-5 Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Mari2012 Serial 99
Permanent link to this record
 

 
Author Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title Linear Constraints as a Modeling Language for Discrete Time Hybrid Systems Type Conference Article
Year 2012 Publication Proceedings of ICSEA 2012, The Seventh International Conference on Software Engineering Advances Abbreviated Journal
Volume Issue (up) Pages 664-671
Keywords
Abstract
Address
Corporate Author Thesis
Publisher ThinkMind 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 @ icsea12 Serial 98
Permanent link to this record
 

 
Author Della Penna, Giuseppe; Di Marco, Antinisca; Intrigila, Benedetto; Melatti, Igor; Pierantonio, Alfonso
Title Xere: Towards a Natural Interoperability between XML and ER Diagrams Type Conference Article
Year 2003 Publication Fundamental Approaches to Software Engineering, 6th International Conference, FASE 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings Abbreviated Journal
Volume Issue (up) Pages 356-371
Keywords
Abstract XML (eXtensible Markup Language) is becoming the standard format for documents on Internet and is widely used to exchange data. Often, the relevant information contained in XML documents needs to be also stored in legacy databases (DB) in order to integrate the new data with the pre-existing ones. In this paper, we introduce a technique for the automatic XML-DB integration, which we call Xere. In particular we present, as the first step of Xere, the mapping algorithm which allows the translation of XML Schemas into Entity-Relationship diagrams.
Address
Corporate Author Thesis
Publisher Springer Place of Publication Editor Pezzè, M.
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 2621 Series Issue Edition
ISSN 3-540-00899-3 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Ddimp03 Serial 86
Permanent link to this record
 

 
Author Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title Automatic Control Software Synthesis for Quantized Discrete Time Hybrid Systems Type Conference Article
Year 2012 Publication Proceedings of the 51th IEEE Conference on Decision and Control, CDC 2012, December 10-13, 2012, Maui, HI, USA Abbreviated Journal
Volume Issue (up) Pages 6120-6125
Keywords
Abstract
Address
Corporate Author Thesis
Publisher IEEE Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN ISBN 978-1-4673-2065-8 Medium
Area Expedition Conference
Notes Techreport version can be found at http://arxiv.org/abs/1207.4098 Approved yes
Call Number Sapienza @ mari @ cdc12 Serial 96
Permanent link to this record
 

 
Author Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico; Alvisi, Lorenzo; Clement, Allen; Li, Harry
Title Model Checking Nash Equilibria in MAD Distributed Systems Type Conference Article
Year 2008 Publication FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design Abbreviated Journal
Volume Issue (up) Pages 1-8
Keywords Model Checking, MAD Distributed System, Nash Equilibrium
Abstract We present a symbolic model checking algorithm for verification of Nash equilibria in finite state mechanisms modeling Multiple Administrative Domains (MAD) distributed systems. Given a finite state mechanism, a proposed protocol for each agent and an indifference threshold for rewards, our model checker returns PASS if the proposed protocol is a Nash equilibrium (up to the given indifference threshold) for the given mechanism, FAIL otherwise. We implemented our model checking algorithm inside the NuSMV model checker and present experimental results showing its effectiveness for moderate size mechanisms. For example, we can handle mechanisms which corresponding normal form games would have more than $10^20$ entries. To the best of our knowledge, no model checking algorithm for verification of mechanism Nash equilibria has been previously published.
Address
Corporate Author Thesis
Publisher IEEE Press Place of Publication Piscataway, NJ, USA Editor Cimatti, A.; Jones, R.
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 978-1-4244-2735-2 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ MarMelSalTroAlvCle08 Serial 93
Permanent link to this record
 

 
Author Della Penna, Giuseppe; Magazzeni, Daniele; Tofani, Alberto; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico
Title Automatic Synthesis of Robust Numerical Controllers Type Conference Article
Year 2007 Publication Icas '07 Abbreviated Journal
Volume Issue (up) Pages 4
Keywords
Abstract A major problem of numerical controllers is their robustness, i.e. the state read from the plant may not be in the controller table, although it may be close to some states in the table. For continuous systems, this problem is typically handled by interpolation techniques. Unfortunately, when the plant contains both continuous and discrete variables, the interpolation approach does not work well. To cope with this kind of systems, we propose a general methodology that exploits explicit model checking in an innovative way to automatically synthesize a (time-) optimal numerical controller from a plant specification and apply an optimized strengthening algorithm only on the most significant states, in order to reach an acceptable robustness degree. We implemented all the algorithms within our CGMurphi tool, an extension of the well-known CMurphi verifier, and tested the effectiveness of our approach by applying it to the well-known truck and trailer obstacles avoidance problem.
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 0-7695-2859-5 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Dmtimt07 Serial 89
Permanent link to this record
 

 
Author Della Penna, Giuseppe; Di Marco, Antinisca; Intrigila, Benedetto; Melatti, Igor; Pierantonio, Alfonso
Title Interoperability mapping from XML schemas to ER diagrams Type Journal Article
Year 2006 Publication Data Knowl. Eng. Abbreviated Journal
Volume 59 Issue (up) 1 Pages 166-188
Keywords
Abstract The eXtensible Markup Language (XML) is a de facto standard on the Internet and is now being used to exchange a variety of data structures. This leads to the problem of efficiently storing, querying and retrieving a great amount of data contained in XML documents. Unfortunately, XML data often need to coexist with historical data. At present, the best solution for storing XML into pre-existing data structures is to extract the information from the XML documents and adapt it to the data structures’ logical model (e.g., the relational model of a DBMS). In this paper, we introduce a technique called Xere (XML entity–relationship exchange) to assist the integration of XML data with other data sources. To this aim, we present an algorithm that maps XML schemas into entity–relationship diagrams, discuss its soundness and completeness and show its implementation in XSLT.
Address
Corporate Author Thesis
Publisher Elsevier Science Publishers B. V. Place of Publication Amsterdam, The Netherlands, The Netherlands Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 0169-023x ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Ddimp06 Serial 77
Permanent link to this record