Refining task specifications using model checking

The problem of schedulability analysis, i.e., determining whether a given task set meets its deadline constraints, has been extensively studied in the real-time systems literature. However, if a task set is not schedulable, then the schedulability analysis results using known techniques (such as utilization-based tests) offer little insight into which task parameters could be changed or refined, in order to make the task set schedulable. To address this problem, we encode the schedulability analysis problem as an equivalent model checking problem. By analyzing the counterexamples reported by the model checker, we discover subsets of values of task parameters that lead to timing violations. We propose a procedure that iteratively refines the task specification by rejecting these subsets, thereby converging towards schedulability. We believe that this approach would be useful for timing debugging of real-time systems, which has received relatively less attention in the literature, especially given its practical relevance.