@Article{Mari_etal2012,
author="Mari, Federico
and Melatti, Igor
and Salvo, Ivano
and Tronci, Enrico",
title="Synthesizing Control Software from Boolean Relations",
journal="International Journal on Advances in Software",
year="2012",
publisher="Iaria",
volume="vol. 5, nr 3\&4",
pages="212--223",
optkeywords="Control Software Synthesis",
optkeywords="Embedded Systems",
optkeywords="Model Checking",
abstract="Many software as well digital hardware automaticsynthesis methods define the set ofimplementations meeting the given systemspecifications with a boolean relation K. Insuch a context a fundamental step in the software(hardware) synthesis process is finding effectivesolutions to the functional equation defined byK. This entails finding a (set of) booleanfunction(s) F (typically represented usingOBDDs, Ordered Binary Decision Diagrams)such that: 1) for all x for which K issatisfiable, K(x, F(x)) = 1 holds; 2) theimplementation of F is efficient with respectto given implementation parameters such as codesize or execution time. While this problem hasbeen widely studied in digital hardware synthesis,little has been done in a software synthesiscontext. Unfortunately, the approaches developedfor hardware synthesis cannot be directly used ina software context. This motivates investigationof effective methods to solve the above problemwhen F has to be implemented with software. Inthis paper, we present an algorithm that, from anOBDD representation for K, generates a C codeimplementation for F that has the same size asthe OBDD for F and a worst case execution timelinear in nr, being n = |x| the number ofinput arguments for functions in F and r thenumber of functions in F. Moreover, a formalproof of the proposed algorithm correctness isalso shown. Finally, we present experimentalresults showing effectiveness of the proposedalgorithm.",
optnote="exported from refbase (http://smarthg.di.uniroma1.it/refbase2/show.php?record=26), last updated on Thu, 07 Nov 2013 15:07:03 +0100",
issn="1942-2628",
file=":http://smarthg.di.uniroma1.it/refbase2/papers/federicomari/2012/26\textit{FedericoMari}etal2012.pdf:PDF"
}