TY  - JOUR
AU  - Mari, Federico
AU  - Melatti, Igor
AU  - Salvo, Ivano
AU  - Tronci, Enrico
ED  - Luigi Lavazza
PY  - 2012
DA  - 2012//
TI  - Synthesizing Control Software from Boolean Relations
T2  - Intern. Journal on Advances in SW
JO  - International Journal on Advances in Software
SP  - 212
EP  - 223
VL  - vol. 5, nr 3&4
PB  - IARIA
KW  - Control Software Synthesis
KW  - Embedded Systems
KW  - Model Checking
AB  - 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.
SN  - 1942-2628
L1  - http://mclab.di.uniroma1.it/publications/papers/federicomari/2012/108_FedericoMari2012.pdf
UR  - http://www.thinkmind.org/index.php?view=article&articleid=soft_v5_n34_2012_6
N1  - exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=108), last updated on Thu, 02 May 2013 11:47:27 +0200
ID  - Mari_etal2012
ER  -