Using Statistical Model Checker for Schedulability Analysis of Real-Time Systems Under Uncertainty

Schedulability analysis aims to decide whether it is possible to meet the timing constraints of the given subset of real-time tasks that will be scheduled by the given policy and executed on the given platform. For some situations (classes of systems and conditions), a guaranteed/proven schedulability analysis method exists. As such a method may be absent for other situations and there may be a practical need to cope with the schedulability analysis in such problematic (but realistic, burdened with uncertainty) situations, the analysis must rely on alternative means. This paper presents some of the situations (related, e.g., to the drift of a clock and OSTime, event/interrupt management, task design patterns or OS components such as a scheduler and task queues) that represent a problem for guaranteed approaches first. Then, it presents our approach for interruptible CPU-based systems; it builds on a simulation model over a network of stochastic timed automata, an instrument able to cope with such situations. To analyze schedulability, we apply the statistical model-checking technique to our model. The technique has already shown to easily scale to complex dynamic systems as well as to efficiently solve various problems. Our results indicate that the model and the technique are appropriate for schedulability analysis in realistic situations, where the computational complexity and result of the analysis are driven by predefined parameters such as the degree of confidence.