On The Discretization And Formalization Of SLDDS Problems

The verification of computer programs has not only been an important issue that has been studied for a long time, but also one of the main driving forces that promotes the development of computer science. Separation logic, a new formal system in this area, is a logical system used to reason about programs that share mutable data structures, whose prominent feature is to support local reasoning and ensure the safety of the programs.Duration calculus is a logical system employed for the design of embedded real-time software system, which is to say that software requirements and characteristics have to be specified with the language in this system before the implementation of the embedded real-time software system, and to be verified after the implementation by using its inference tool.At present, researchers on the real-time task scheduling theory pay more attention to the problems of real-time restriction rather than that of space restriction; however, in many practical problems such as controlling of railway crossing, network service congestion, city traffic control, and shared resource software system, etc., space is an indispensable factor. Although duration calculus is a powerful tool on specifying real-time system, it does not consider the space factor; and separation logic works well on the spatial sharing problems, but not the synchronization of concurrent processes. Therefore, by introducing the language of separation logic to duration calculus, we can formalize the scheduling problems of real-time process with space restrictions and determine the solvability of the scheduling problems mechanically.In this thesis, we design a mathematical model of SLDDS on the background of practical problem, we also study the scheduling problem in the model, and finally, we present the formalization of the model.The main contents of this thesis are presented as the follows:Preface: a review of separation logic and duration calculus and main idea of this paper.Chapter I: an introduction to basic separation logic.Chapter II: an introduction to duration calculus.Chapter III: at first, we extend DDS model to SLDDS model; then we reconsider Liu-Layland's theorem, discuss the discretization problems of real-time schedules; finally, we will give a sufficient and necessary condition for schedulability of SLDDS problems.Chapter IV: an introduction to the languages we need to use, and then a preliminary study of the formalization of SLDDS models.The main theorems are as follows:Theorem 3.1 Given a problem of SLDDS, is schedulable if and only if their is a Q Q division of such that }All of the small stripes {d i×ai |1≤i≤n can be put into the rectangle D×1 in the way that the following conditions are satisfied:(ⅰ) All of the stripes must be vertical and not overlapped;(ⅱ)Any two stripes of the same parameters d i×Wi can not be vertically lined. That is to say, any vertical lines through points at the bottom of the rectangle D×1may meet at most one stripe with the same parameters d i×Wi.Theorem 3.2 For a problem of SLDDS, is schedulable if and only if their is a step function f ( t ) over [0, 1] such that(ⅰ) f ( t )≤D for all t∈[0,1];Theorem 3.3 In SLDDS model, SLEDF scheduling algorithm is optimal. That is, if a SLDDS question is schedulable, then it can be scheduled by SLEDF algorithm.