Modeling of Energy Autonomous Systems: Video Decoding Application (Joint with

title:Modeling of Energy Autonomous Systems: Video Decoding Application (Joint with
company:Joint with EU project SENSATION and company RECORE systems
keywords:Data flow, timed automata, Video Decoding Application, multi-core Soc
contact:W. Ahmad MSc & Prof.dr. M.I.A. Stoelinga & prof.dr. J.C. van de Pol
to be started:as soon as possible


In embedded systems, energy efficiency has always been a central concern. Work has always been directed at changing the hardware or tooling for software development to use less energy, while still delivering sufficient compute power and communication capacity for the applications that we want to run. In other words, application engineers have been kept out of the proverbial wind.

Because applications become more complex and, thereby, less predictable, the low-hanging fruit for battery life extension is a change in application engineering. In the European research project Sensation, we are looking at how to make systems energy autonomous. This means that the level of energy stored in a battery ‘now’ and – if a device has ways of harvesting energy, like a solar panel – the expected available energy in the future should be taken into account when making decisions. Different model-checking techniques such as (priced) timed automata, probabilistic timed automata and (priced) Markov automata. provide sufficient logics and semantics to model such behaviour.

The central question for this Master’s assignment is whether we can design applications in such a way that the (expected) available energy changes the level of service of an application. At Recore Systems, application platforms are being designed for the cutting edge market of low-power, high-service systems. Together with the University of Twente, Recore is exploring their Video Decoding application mapped on a state-of-the-art SoC as a use-case for this exploration. We are looking for a student to explore different approaches to modelling the behaviour of this application, in the context of energy-driven choices regarding the level of service. As such, we are offering a student a chance to participate at the bleeding edge of the field of embedded systems.


1. Study different formalisms such as (priced) timed automata, probabilistic timed automata and (priced) Markov automata.

2. Study the case-study provided by Recore Systems

3. Model the case-study using different model-checking formalisms

4. Analyse the results and implementation

 The project will be done in collaboration with Recore Systems and will require frequent visits to their office in Enschede. Thus, the student will get a chance to work both in an industrial and academic environment.