Home | << 1 2 3 4 5 6 7 >> |
Records | |||||
---|---|---|---|---|---|
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; Tronci, Enrico; Finzi, Alberto | ||||
Title | A multi-hop advertising discovery and delivering protocol for multi administrative domain MANET | Type | Journal Article | ||
Year | 2013 | Publication | Mobile Information Systems | Abbreviated Journal | Mobile Information Systems |
Volume | 3 | Issue | 9 | Pages | 261-280 |
Keywords | |||||
Abstract | |||||
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 | 1574-017x (Print) 1875-905X (Online) | ISBN | Medium | ||
Area | Expedition | Conference | |||
Notes | Approved | no | |||
Call Number | Sapienza @ melatti @ | Serial | 109 | ||
Permanent link to this record | |||||
Author | Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico | ||||
Title | Model Based Synthesis of Control Software from System Level Formal Specifications | Type | Journal Article | ||
Year | 2014 | Publication | ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY | Abbreviated Journal | ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY |
Volume | 23 | Issue | 1 | Pages | Article 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 | no | |||
Call Number | Sapienza @ melatti @ | Serial | 110 | ||
Permanent link to this record |