Model-based energy analysis of battery powered systems

The use of mobile devices is often limited by the lifetime of the included batteries. This lifetime naturally depends on the battery’s capacity and on the rate at which the battery is discharged. However, it also depends on the usage pattern, i.e., the workload, of the battery. When a battery is continuously discharged, a high current will cause it to provide less energy until the end of its lifetime than a lower current. This effect is termed the rate-capacity effect. On the other hand, during periods of low or no discharge current, the battery can recover to a certain extent. This effect is termed the recovery effect. In order to investigate the influence of the device workload on the battery lifetime a battery model is needed that includes the above described effects. Many different battery models have been developed for different application areas. We make a comparison of the main approaches that have been taken. Analytical models appear to be the best suited to use in combination with a device workload model, in particular, the so-called kinetic battery model. This model is combined with a continuous-time Markov chain, which models the workload of a battery powered device in a stochastic manner. For this model, we have developed algorithms to compute both the distribution and expected value of the battery lifetime and the charge delivered by the battery. These algorithms are used to make comparisons between different workloads, and can be used to analyse their impact on the system lifetime. In a system where multiple batteries can be connected, battery scheduling can be used to “spread” the workload over the individual batteries. Two approaches have been taken to find the optimal schedule for a given load. In the first approach scheduling decisions are only taken when a change in the workload occurs. The kinetic battery model is incorporated into a priced-timed automata model, and we use the model checking tool Uppaal Cora to find schedules that lead to the longest system lifetime. The second approach is an analytical one, in which scheduling decisions can be made at any point in time, that is, independently of workload changes. The analysis of the equations of the kinetic battery model provides an upper bound for the battery lifetime. This upper bound can be approached with any type of scheduler, as long as one can switch fast enough. Both the approaches show that battery scheduling can potentially provide a considerable improvement of the system lifetime. The actual improvement mainly depends on the ratio between the battery capacity and the average discharge current.