The Inverse Method: Parametric Verification of Real-time Embedded Systems

6

Application to the Robustness Analysis of Scheduling Problems

In this chapter, we use the inverse method for timed automata introduced in Chapter 2 to analyze specifically the robustness of real-time scheduling systems. Furthermore, we use the behavioral cartography of Chapter 4 to synthesize schedulable zones of real-time systems. More precisely, we are interested here in representing and analyzing the schedulability region, that is the region of parameter space that corresponds to a feasible design.

Outline of the chapter

Preliminary definitions are introduced in section 6.1. In section 6.2, we explain through an example the principle of the application of the inverse method to scheduling problems. In section 6.3, we apply the method to various schedulability problems of the literature (jobs with variable execution times, deadlines), as well as to an industrial case study. The results are discussed in section 6.4. Related work is discussed in section 6.5.

6.1. Preliminaries

6.1.1. Scheduling problems

A real-time system is viewed in this chapter as a set of jobs {J₁, J₂, … , J_n}. A job J_i generates a possibly infinite stream of tasks {J_i,1, J_i,2, … }. When a job is activated, it executes for at most time C_i, and has to terminate within the relative deadline D_i. Some real-time systems feature a pre-emption mechanism: tasks may have a different priority. When a low-priority task ...