Synthesizing Control Software from Boolean Relations
Mari
Federico
author
Melatti
Igor
author
Salvo
Ivano
author
Tronci
Enrico
author
2012
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.
Control Software Synthesis
Embedded Systems
Model Checking
exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=108), last updated on Thu, 02 May 2013 11:47:27 +0200
text
http://www.thinkmind.org/index.php?view=article&articleid=soft_v5_n34_2012_6
http://mclab.di.uniroma1.it/publications/papers/federicomari/2012/108_FedericoMari2012.pdf
http://www.thinkmind.org/index.php?view=article&articleid=soft_v5_n34_2012_6
Mari_etal2012
International Journal on Advances in Software
Intern. Journal on Advances in SW
Luigi Lavazza
editor
2012
IARIA
continuing
periodical
academic journal
vol. 5, nr 3&4
212
223
1942-2628