Home | << 1 2 3 4 5 6 7 >> |
Records | |||||
---|---|---|---|---|---|
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 | Edition | |||
ISSN | 1942-2628 | ISBN | Medium | ||
Area | Expedition | Conference | |||
Notes | Approved | yes | |||
Call Number | Sapienza @ melatti @ | Serial | 115 | ||
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 | 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 | |||||
Author | Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico | ||||
Title | Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems | Type | Conference Article | ||
Year | 2010 | Publication | Computer Aided Verification | Abbreviated Journal | |
Volume | Issue | Pages | 180-195 | ||
Keywords | |||||
Abstract | We present an algorithm that given a Discrete Time Linear Hybrid System returns a correct-by-construction software implementation K for a (near time optimal) robust quantized feedback controller for along with the set of states on which K is guaranteed to work correctly (controllable region). Furthermore, K has a Worst Case Execution Time linear in the number of bits of the quantization schema. | ||||
Address | |||||
Corporate Author | Thesis | ||||
Publisher | Springer Berlin / Heidelberg | Place of Publication | Editor | Touili, T.; Cook, B.; Jackson, P. | |
Language | Summary Language | Original Title | |||
Series Editor | Series Title | Lecture Notes in Computer Science | Abbreviated Series Title | ||
Series Volume | 6174 | Series Issue | Edition | ||
ISSN | ISBN | Medium | |||
Area | Expedition | Conference | |||
Notes | Approved | yes | |||
Call Number | Sapienza @ mari @ cav2010 | Serial | 16 | ||
Permanent link to this record | |||||
Author | Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico | ||||
Title | Synthesizing Control Software from Boolean Relations | Type | Journal Article | ||
Year | 2012 | Publication | International Journal on Advances in Software | Abbreviated Journal | Intern. Journal on Advances in SW |
Volume | vol. 5, nr 3&4 | Issue | Pages | 212-223 | |
Keywords | Control Software Synthesis; Embedded Systems; Model Checking | ||||
Abstract | Many software as well digital hardware automatic
synthesis methods define the set of implementations meeting the given system specifications with a boolean relation K. In such a context a fundamental step in the software (hardware) synthesis process is finding effective solutions to the functional equation defined by K. This entails finding a (set of) boolean function(s) F (typically represented using OBDDs, Ordered Binary Decision Diagrams) such that: 1) for all x for which K is satisfiable, K(x, F(x)) = 1 holds; 2) the implementation of F is efficient with respect to given implementation parameters such as code size or execution time. While this problem has been widely studied in digital hardware synthesis, little has been done in a software synthesis context. Unfortunately, the approaches developed for hardware synthesis cannot be directly used in a software context. This motivates investigation of effective methods to solve the above problem when F has to be implemented with software. In this paper, we present an algorithm that, from an OBDD representation for K, generates a C code implementation for F that has the same size as the OBDD for F and a worst case execution time linear in nr, being n = |x| the number of input arguments for functions in F and r the number of functions in F. Moreover, a formal proof of the proposed algorithm correctness is also shown. Finally, we present experimental results showing effectiveness of the proposed algorithm. |
||||
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 | Edition | |||
ISSN | 1942-2628 | ISBN | Medium | ||
Area | Expedition | Conference | |||
Notes | Approved | yes | |||
Call Number | Sapienza @ melatti @ | Serial | 108 | ||
Permanent link to this record | |||||
Author | Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa | ||||
Title | Bounded Probabilistic Model Checking with the Mur$\varphi$ Verifier | Type | Conference Article | ||
Year | 2004 | Publication | Formal Methods in Computer-Aided Design, 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings | Abbreviated Journal | |
Volume | Issue | Pages | 214-229 | ||
Keywords | |||||
Abstract | In this paper we present an explicit verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. We restrict ourselves to verification of Bounded PCTL formulas (BPCTL), that is, PCTL formulas in which all Until operators are bounded, possibly with different bounds. This means that we consider only paths (system runs) of bounded length. Given a Markov Chain $\cal M$ and a BPCTL formula Φ, our algorithm checks if Φ is satisfied in $\cal M$. This allows to verify important properties, such as reliability in Discrete Time Hybrid Systems. We present an implementation of our algorithm within a suitable extension of the Mur$\varphi$ verifier. We call FHP-Mur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$) such extension of the Mur$\varphi$ verifier. We give experimental results comparing FHP-Mur$\varphi$ with (a finite horizon subset of) PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHP-Mur$\varphi$ can effectively handle verification of BPCTL formulas for systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems). | ||||
Address | |||||
Corporate Author | Thesis | ||||
Publisher | Springer | Place of Publication | Editor | Hu, A.J.; Martin, A.K. | |
Language | Summary Language | Original Title | |||
Series Editor | Series Title | Lecture Notes in Computer Science | Abbreviated Series Title | ||
Series Volume | 3312 | Series Issue | Edition | ||
ISSN | 3-540-23738-0 | ISBN | Medium | ||
Area | Expedition | Conference | |||
Notes | Approved | yes | |||
Call Number | Sapienza @ mari @ Dimtz04 | Serial | 87 | ||
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. | ||||
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 | 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 | Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico | ||||
Title | On Model Based Synthesis of Embedded Control Software | Type | Conference Article | ||
Year | 2012 | Publication | Proceedings of the 12th International Conference on Embedded Software, EMSOFT 2012, part of the Eighth Embedded Systems Week, ESWeek 2012, Tampere, Finland, October 7-12, 2012 | Abbreviated Journal | |
Volume | Issue | Pages | 227-236 | ||
Keywords | |||||
Abstract | |||||
Address | |||||
Corporate Author | Thesis | ||||
Publisher | ACM | Place of Publication | Editor | Ahmed Jerraya and Luca P. Carloni and Florence Maraninchi and John Regehr | |
Language | Summary Language | Original Title | |||
Series Editor | Series Title | Abbreviated Series Title | |||
Series Volume | Series Issue | Edition | |||
ISSN | ISBN | 978-1-4503-1425-1 | Medium | ||
Area | Expedition | Conference | |||
Notes | Techreport version can be found at arxiv.org | Approved | yes | ||
Call Number | Sapienza @ mari @ emsoft12 | Serial | 97 | ||
Permanent link to this record | |||||
Author | Chen, Q.M.; Finzi, A.; Mancini, T.; Melatti, I.; Tronci, E. | ||||
Title | MILP, Pseudo-Boolean, and OMT Solvers for Optimal Fault-Tolerant Placements of Relay Nodes in Mission Critical Wireless Networks | Type | Journal Article | ||
Year | 2020 | Publication | Abbreviated Journal | Fundamenta Informaticae | |
Volume | 174 | Issue | Pages | 229-258 | |
Keywords | |||||
Abstract | In critical infrastructures like airports, much care has to be devoted in protecting radio communication networks from external electromagnetic interference. Protection of such mission-critical radio communication networks is usually tackled by exploiting radiogoniometers: at least three suitably deployed radiogoniometers, and a gateway gathering information from them, permit to monitor and localise sources of electromagnetic emissions that are not supposed to be present in the monitored area. Typically, radiogoniometers are connected to the gateway through relay nodes . As a result, some degree of fault-tolerance for the network of relay nodes is essential in order to offer a reliable monitoring. On the other hand, deployment of relay nodes is typically quite expensive. As a result, we have two conflicting requirements: minimise costs while guaranteeing a given fault-tolerance. In this paper, we address the problem of computing a deployment for relay nodes that minimises the overall cost while at the same time guaranteeing proper working of the network even when some of the relay nodes (up to a given maximum number) become faulty (fault-tolerance ). We show that, by means of a computation-intensive pre-processing on a HPC infrastructure, the above optimisation problem can be encoded as a 0/1 Linear Program, becoming suitable to be approached with standard Artificial Intelligence reasoners like MILP, PB-SAT, and SMT/OMT solvers. Our problem formulation enables us to present experimental results comparing the performance of these three solving technologies on a real case study of a relay node network deployment in areas of the Leonardo da Vinci Airport in Rome, Italy. | ||||
Address | |||||
Corporate Author | Thesis | ||||
Publisher | IOS Press | Place of Publication | Editor | ||
Language | Summary Language | Original Title | |||
Series Editor | Series Title | Abbreviated Series Title | |||
Series Volume | Series Issue | Edition | |||
ISSN | 1875-8681 | ISBN | Medium | ||
Area | Expedition | Conference | |||
Notes | Approved | no | |||
Call Number | MCLab @ davi @ | Serial | 188 | ||
Permanent link to this record | |||||
Author | Intrigila, Benedetto; Melatti, Igor; Tofani, Alberto; Macchiarelli, Guido | ||||
Title | Computational models of myocardial endomysial collagen arrangement | Type | Journal Article | ||
Year | 2007 | Publication | Computer Methods and Programs in Biomedicine | Abbreviated Journal | |
Volume | 86 | Issue | 3 | Pages | 232-244 |
Keywords | |||||
Abstract | Collagen extracellular matrix is one of the factors related to high passive stiffness of cardiac muscle. However, the architecture and the mechanical aspects of the cardiac collagen matrix are not completely known. In particular, endomysial collagen contribution to the passive mechanics of cardiac muscle as well as its micro anatomical arrangement is still a matter of debate. In order to investigate mechanical and structural properties of endomysial collagen, we consider two alternative computational models of some specific aspects of the cardiac muscle. These two models represent two different views of endomysial collagen distribution: (1) the traditional view and (2) a new view suggested by the data obtained from scanning electron microscopy (SEM) in NaOH macerated samples (a method for isolating collagen from the other tissue). We model the myocardial tissue as a net of spring elements representing the cardiomyocytes together with the endomysial collagen distribution. Each element is a viscous elastic spring, characterized by an elastic and a viscous constant. We connect these springs to imitate the interconnections between collagen fibers. Then we apply to the net of springs some external forces of suitable magnitude and direction, obtaining an extension of the net itself. In our setting, the ratio forces magnitude /net extension is intended to model the stress /strain ratio of a microscopical portion of the myocardial tissue. To solve the problem of the correct identification of the values of the different parameters involved, we use an artificial neural network approach. In particular, we use this technique to learn, given a distribution of external forces, the elastic constants of the springs needed to obtain a desired extension as an equilibrium position. Our experimental findings show that, in the model of collagen distribution structured according to the new view, a given stress /strain ratio (of the net of springs, in the sense specified above) is obtained with much smaller (w.r.t. the other model, corresponding to the traditional view) elasticity constants of the springs. This seems to indicate that by an appropriate structure, a given stiffness of the myocardial tissue can be obtained with endomysial collagen fibers of much smaller size. | ||||
Address | |||||
Corporate Author | Thesis | ||||
Publisher | Elsevier North-Holland, Inc. | Place of Publication | New York, NY, USA | Editor | |
Language | Summary Language | Original Title | |||
Series Editor | Series Title | Abbreviated Series Title | |||
Series Volume | Series Issue | Edition | |||
ISSN | 0169-2607 | ISBN | Medium | ||
Area | Expedition | Conference | |||
Notes | Approved | yes | |||
Call Number | Sapienza @ mari @ Imtm07 | Serial | 82 | ||
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 | 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 |