Synchronous dataflow (SDF) graphs are a widely used formalism for modelling, analysing and realising streaming applications, both on a single processor and in a multiprocessing context. Efficient schedules are essential to obtain maximal throughput under the constraint of available number of resources. This paper presents an approach to schedule SDF graphs using a proven formalism of timed automata (TA). TA maintain a good balance between expressiveness and tractability, and are supported by powerful verification tools, e.g. Uppaal. We describe a compositional translation of SDF graphs to TA, and analysis and verification in the Uppaal state-of-the-art tool. This approach does not require any transformation of SDF graphs and helps to find schedules with a compromise between the number of processors required and the throughput. It also allows quantitative model checking and verification of user-defined properties such as the absence of deadlocks, safety, liveness and throughput analysis. This translation also forms the basis for future work to extend this analysis of SDF graphs with new features such as stochastics, energy consumption and costs.
|Place of Publication||Enschede|
|Publisher||Centre for Telematics and Information Technology (CTIT)|
|Number of pages||32|
|Publication status||Published - 21 Jan 2014|
|Name||CTIT Technical Report Series|
|Publisher||University of Twente, Centre for Telematics and Information Technology|
- Timed Automata
- EC Grant Agreement nr.: FP7/318490
- Synchronous Dataflow Graph
- EC Grant Agreement nr.: FP7/2007-2013
Ahmad, W., de Groote, R., Holzenspies, P. K. F., Stoelinga, M. I. A., & van de Pol, J. C. (2014). Resource-constrained optimal scheduling of synchronous dataflow graphs via timed automata. (CTIT Technical Report Series; No. TR-CTIT-13-17). Enschede: Centre for Telematics and Information Technology (CTIT).