A Satisfi ability Approach to Speed Assignment for Distributed Real-Time Systems
Pratyush Kumar, Devesh Chokshi, and Lothar Thiele.
In In Proceedings of the 2013 Design, Automation & Test in Europe Conference & Exhibition, DATE 2013, Grenoble, France, March 2013. IEEE.
We study the problem of assigning speeds to resources serving distributed applications with delay, buff er and energy constraints. We argue that the considered problem does not have any straightforward solution due to the intricately related constraints. As a solution, we propose using Real-Time Calculus (RTC) to analyse the constraints and a SATis fiability solver to efficiently explore the design space. To this end, we develop an SMT solver by using the OpenSMT framework and the modular Performance Analysis (MPA) toolbox. Two key enablers for this implementation are the analysis of incomplete models and generation of conflict clauses in RTC. The results on problem instances with very large decision spaces indicate that the proposed SMT solver performs very well in practice.
