|
doi: 10.3850/978-3-9815370-4-8_0606
A Symbolic System Synthesis Approach for Hard Real-Time Systems Based on Coordinated SMT-Solving
Alexander Biewer1, Benjamin Andres2, Jens Gladigau1, Torsten Schaub2 and Christian Haubelt3
1Corporate Sector Research, Robert Bosch GmbH, Germany
2Knowledge Processing and Information Systems, University of Potsdam, Germany
3Applied Microelectronics and Computer Engineering, University of Rostock, Germany
ABSTRACT
We propose an SMT-based system synthesis approach where the logic solver performs static binding and routing while the background theory solver computes global time-triggered schedules. In contrast to previous work, we assign additional time to the logic solver in order to refine the binding and routing such that the background theory solver is more likely to find a feasible schedule within a reasonable amount of time. We show by experiments that this coordination of the two solvers results in a considerable reduction of the overall synthesis time.
Full Text (PDF)
|