O'Reilly logo

The Inverse Method: Parametric Verification of Real-time Embedded Systems by Romain Soulat, Etienne André

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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 image is viewed in this chapter as a set of jobs {J1, J2, … , Jn}. A job Ji generates a possibly infinite stream of tasks {Ji,1, Ji,2, … }. When a job is activated, it executes for at most time Ci, and has to terminate within the relative deadline Di. Some real-time systems feature a pre-emption mechanism: tasks may have a different priority. When a low-priority task ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required