Home // International Journal On Advances in Software, volume 5, numbers 3 and 4, 2012 // View article

Synthesizing Control Software from Boolean Relations

Authors:
Federico Mari
Igor Melatti
Ivano Salvo
Enrico Tronci

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.

Pages: 212 to 223

Copyright: Copyright (c) to authors, 2012. Used with permission.

Publication date: December 31, 2012

Published in: journal

ISSN: 1942-2628