The Parallel Model Of DDS And Its Formalization

DDS (Deadline-driven scheduler) is a classical scheduling algorithm of real-time systems. Based on the original framework of DDS, we form the parallel model of DDS by adding the condition of space-constraint. In this model, multiprocessor task scheduling is investigated, and the primary scheduling algorithm and the general scheduling algorithm are presented too. In order to formalize the parallel model of DDS, we firstly introduce duration calculus with which we can formalize DDS model. Because of the space-constraint, duration calculus is not enough to formalize the parallel model of DDS. As separation logic can express the space-separation successfully, we then introduce the syntax and semantics of separation logic, a formalizing proof of bubble sort algorithm by using separation logic are presented too. After that, we extend duration calculus to DC* with the idea of separation logic, and the formalization of the parallel model of DDS is given in this paper.The structure of the paper is following:Chapter 1 is the research background of the paper. We introduce some major achievements of real-time systems and the history of duration calculus and separation logic.Chapter 2 is about the parallel model of DDS. Based on our extension of original framework of DDS, multiprocessor task scheduling with space-constraint is investigated. While studying the parallel model of DDS, we present the concept of maximal separated task-set, the primary scheduling algorithm, general scheduling algorithm and the condition if general scheduling algorithm is feasible.The main conclusions of chapter 2 are the following:Theorem2.2 For a given maximal separated task-set , there is a primary scheduling algorithm of .Theorem2.3 Assume that is a division of task-set and for each , is its primary task. The general scheduling algorithm is feasible if and only if the set of primary tasksIn Chapter 3 the syntax and semantics of Duration Calculus are present.In Chapter 4 we systematically introduce the logical settings of Separation Logic, including its syntax and semantics. As an applying example of separation logic, we also give a formalizing proof of Bubble Sort algorithm by using separation logic. Chapter 5 is mainly about the formalization of the parallel model of DDS. We extend Duration Calculus to DC~* with the idea of separation logic, and the formalization of DDS parallel model under DC~* is given in this chapter.Chapter 6 is the summarization and the future research direction.