Abstract: Synchronous dataflow graphs (SDFGs) are widely used to model streaming applications such as multimedia and digital signal processing applications.Streaming applications are usually required to reach a high throughput to guarantee smooth running.Using heterogeneous multicore processors to improve the throughput of streaming applications has become a feasible solution.However,a higher throughput is usually achieved with the increase of energy consumption.We presented a method to explore the Pareto space of energy consumption and throughput and find the schedule of each Pareto point.A system model includes an SDFG description for the application and a heterogeneous multicore platform.The system model is transformed to a network of timed automata (NTA) and the optimization goals are formalized as temporal logic formulae.The NTA and formulae are then used as the input of the real time model checking tool UPPAAL.The Pareto points and corresponding schedules by the trace provided by UPPAAL can be obtained.Our method is exact,which is benefited from the exhaustive search nature of model checking technique.The method can be used to help designers to understand the quantitative relationship between energy consumption and throughput in the design period,shortening development cycles and reducing costs of system developments.

Key words: Synchronous dataflow graphs,Heterogeneous multicore platform,Pareto optimization,Scheduling,Model checking