Cost-optimal timed trace synthesis for scheduling of intermittent embedded systems

Intermittent computing is an emerging paradigm for systems without batteries and powered by intermittent energy sources. This paradigm promises a more energy-efficient design of computing systems. It seems particularly well suited to the field of connected sensors that form the first level of the Internet of Things. This application domain requires a reactive computing model. The definition of an intermittent and reactive model is a problem that has not yet been fully explored in the literature. In this paper, we focus on the modeling and analysis of intermittent reactive systems. We first introduce an extension of Time Petri Nets with cost to model the different dimensions of the system: concurrency, real time, energy consumption and reward representing the gains generated by the system when it has succeeded in carrying out certain actions. We then aim to synthesize optimal runs of the model that achieve the highest possible reward under a given cost (energy) constraint. We propose a symbolic algorithm for constrained-cost state space computation and prove its termination. We then present algorithms for the synthesis of the optimal traces from an exhaustive or partial state space exploration. We finally illustrate the cost-optimal traces synthesis on a case study and show how that can be used online for joint management of computing time and energy.