| Home | << 1 2 3 4 5 6 7 8 9 10 >> [11–13] |
|
| Records | |||||
|---|---|---|---|---|---|
| Author | Böhm, Corrado; Tronci, Enrico | ||||
| Title | X-Separability and Left-Invertibility in lambda-calculus | Type | Conference Article | ||
| Year | 1987 | Publication | Symposium on Logic in Computer Science (LICS) | Abbreviated Journal | |
| Volume | Issue | Pages | 320-328 | ||
| Keywords | |||||
| Abstract | |||||
| Address | |||||
| Corporate Author | Thesis | ||||
Publisher  |
IEEE Computer Society | Place of Publication | Ithaca, New York, USA | 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 @ lics87 | Serial | 63 | ||
| Permanent link to this record | |||||
| Author | Tronci, Enrico | ||||
| Title | On Computing Optimal Controllers for Finite State Systems | Type | Conference Article | ||
| Year | 1997 | Publication | CDC '97: Proceedings of the 36th IEEE International Conference on Decision and Control | Abbreviated Journal | |
| Volume | Issue | Pages | |||
| Keywords | |||||
| Abstract | |||||
| Address | |||||
| Corporate Author | Thesis | ||||
| Publisher |
IEEE Computer Society | Place of Publication | Washington, DC, USA | 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 @ cdc97 | Serial | 66 | ||
| Permanent link to this record | |||||
| Author | Tronci, Enrico | ||||
| Title | Optimal Finite State Supervisory Control | Type | Conference Article | ||
| Year | 1996 | Publication | CDC '96: Proceedings of the 35th IEEE International Conference on Decision and Control | Abbreviated Journal | |
| Volume | Issue | Pages | |||
| Keywords | |||||
| Abstract | Supervisory Controllers are Discrete Event Dynamic Systems (DEDSs) forming the discrete core of a Hybrid Control System. We address the problem of automatic synthesis of Optimal Finite State Supervisory Controllers (OSCs). We show that Boolean First Order Logic (BFOL) and Binary Decision Diagrams (BDDs) are an effective methodological and practical framework for Optimal Finite State Supervisory Control. Using BFOL programs (i.e. systems of boolean functional equations) and BDDs we give a symbolic (i.e. BDD based) algorithm for automatic synthesis of OSCs. Our OSC synthesis algorithm can handle arbitrary sets of final states as well as plant transition relations containing loops and uncontrollable events (e.g. failures). We report on experimental results on the use of our OSC synthesis algorithm to synthesize a C program implementing a minimum fuel OSC for two autonomous vehicles moving on a 4 x 4 grid. | ||||
| Address | |||||
| Corporate Author | Thesis | ||||
| Publisher |
IEEE Computer Society | Place of Publication | Washington, DC, USA | 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 @ cdc96 | Serial | 67 | ||
| Permanent link to this record | |||||
| Author | Intrigila, Benedetto; Magazzeni, Daniele; Melatti, Igor; Tronci, Enrico | ||||
| Title | A Model Checking Technique for the Verification of Fuzzy Control Systems | Type | Conference Article | ||
| Year | 2005 | Publication | CIMCA '05: Proceedings of the International Conference on Computational Intelligence for Modelling, Control and Automation and International Conference on Intelligent Agents, Web Technologies and Internet Commerce Vol-1 (CIMCA-IAWTIC'06) | Abbreviated Journal | |
| Volume | Issue | Pages | 536-542 | ||
| Keywords | |||||
| Abstract | Fuzzy control is well known as a powerful technique for designing and realizing control systems. However, statistical evidence for their correct behavior may be not enough, even when it is based on a large number of samplings. In order to provide a more systematic verification process, the cell-to-cell mapping technology has been used in a number of cases as a verification tool for fuzzy control systems and, more recently, to assess their optimality and robustness. However, cell-to-cell mapping is typically limited in the number of cells it can explore. To overcome this limitation, in this paper we show how model checking techniques may be instead used to verify the correct behavior of a fuzzy control system. To this end, we use a modified version of theMurphi verifier, which ease the modeling phase by allowing to use finite precision real numbers and external C functions. In this way, also already designed simulators may be used for the verification phase. With respect to the cell mapping technique, our approach appears to be complementary; indeed, it explores a much larger number of states, at the cost of being less informative on the global dynamic of the system. | ||||
| Address | |||||
| Corporate Author | Thesis | ||||
| Publisher |
IEEE Computer Society | Place of Publication | Washington, DC, USA | Editor | |
| Language | Summary Language | Original Title | |||
| Series Editor | Series Title | Abbreviated Series Title | |||
| Series Volume | Series Issue | Edition | |||
| ISSN | 0-7695-2504-0-01 | ISBN | Medium | ||
| Area | Expedition | Conference | |||
| Notes | Approved | yes | |||
| Call Number | Sapienza @ mari @ Immt05 | Serial | 75 | ||
| Permanent link to this record | |||||
| Author | Brizzolari, Francesco; Melatti, Igor; Tronci, Enrico; Della Penna, Giuseppe | ||||
| Title | Disk Based Software Verification via Bounded Model Checking | Type | Conference Article | ||
| Year | 2007 | Publication | APSEC '07: Proceedings of the 14th Asia-Pacific Software Engineering Conference | Abbreviated Journal | |
| Volume | Issue | Pages | 358-365 | ||
| Keywords | |||||
| Abstract | One of the most successful approach to automatic software verification is SAT based bounded model checking (BMC). One of the main factors limiting the size of programs that can be automatically verified via BMC is the huge number of clauses that the backend SAT solver has to process. In fact, because of this, the SAT solver may easily run out of RAM. We present two disk based algorithms that can considerably decrease the number of clauses that a BMC backend SAT solver has to process in RAM. Our experimental results show that using our disk based algorithms we can automatically verify programs that are out of reach for RAM based BMC. | ||||
| Address | |||||
| Corporate Author | Thesis | ||||
| Publisher |
IEEE Computer Society | Place of Publication | Washington, DC, USA | Editor | |
| Language | Summary Language | Original Title | |||
| Series Editor | Series Title | Abbreviated Series Title | |||
| Series Volume | Series Issue | Edition | |||
| ISSN | 0-7695-3057-5 | ISBN | Medium | ||
| Area | Expedition | Conference | |||
| Notes | Approved | yes | |||
| Call Number | Sapienza @ mari @ Bmtd07 | Serial | 76 | ||
| 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 | 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 | 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 | Edition | |||
| ISSN | ISBN | Medium | |||
| Area | Expedition | Conference | |||
| Notes | Approved | no | |||
| Call Number | Sapienza @ melatti @ | Serial | 118 | ||
| 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 | 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 | ||||
| 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 | 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 | |||||