Models And Formalization Of Concurrent Real-time Systems

In our understanding, a real-time system is a computational system with real-time requirements.We first introduce the development of general real-time system In chapterⅠ. Researchers in the real time system mainly consider the scheduling problems on the periodical processes (tasks) with periodical deadlines. The results in this area include valid scheduling algorithms under the framework that there is only one processor, theorems on algorithm discussions such as the famous Liu-Layland theorem.In chapterⅡ, we introducing the space factor and multi-processors, present an extended framework of real-time systems. Each process needs a certain amount of space, sayνi ( t). It is a real value function of the time variable t. But in the general, the total amount of space, D, is limited. In this extended framework, the parallel and concurrent processes can be clearly interpreted and the valid algorithms can be established.In chapterⅢ,we define parallel models : when (?) i ,(1≤i≤m) ,νi( t) is a constant function of t , i.e. (?) d i∈(?),ν(i t) = di. We use the language of duration calculus and separation logic to present the formalization of this parallel models . We introduce the concept of space separation of processes. Assume that for each process Pi , the ratio of its space requirement is ri= dDi. Denote a subset of {1 ,2, , m} asΔ. if∑r j≤1,j∈Δ, then we call it space separable. There are finitely many of them, we denote each of them asΔs , s∈I. We writeεs=∑r j, j∈Δs for each such a subset. Consider a step function: obtain the following theorem:Theorem 3.1For the given parallel model, three is a valid scheduling algorithm if and only if there is a step functionIn chapterⅣ,we define concurrent models ,and use the language of process algebra to present the formalization of this concurrent model. When the space occupancy function vi ( t ) is variable for each i , we obtain concurrent models of real-time processes. In this paper, we construct a basic concurrent model LCM (Linear Concurrent Model): Let D = 1, k≥2 is a fixed integer, for each Pi ,the time interval of this process being processed in the jth periodical time requirement. We also assume that for each process, when it starts to be processed, it will not stop until the process has been completed. The space occupancy function is defined as following for each i:We also define the time-space occupancy for each process over the time interval vi t.Our goal is to find algorithms in this model that the efficiency ratio is much larger than 12 . Consider the following"greedy algorithm":1. When t = 0, we start processing k processes simultaneously.2. Each process will not stop until it has been completed.3. Whenever an amount of free space has been released, we start a new process.To understand the possible maximal time-space efficiency of this greedy algorithm, and to see the cutting points of this scheduling, we use MAPLE to make a program. Base on this grogram, we had made the conjecture that the time-space efficiency rate of greedy algorithm is . This experiment leads to the following theorem:Theorem 4.1In this concurrent model LCM, is the maximal up-bound of the time-space efficiency rates of valid scheduling algorithms.But the above program also shows that the control of the greedy algorithm is complicated. Therefore we have designed a simple cyclic algorithm with the same efficiency rate:1. When t = 0, we start only one process, say P1 .2. When , n is an int eger, 0 < n < 2 k- 1, we start a new process P_{n +1} .3. When t = 1, P1 has just being finished, and the total amount of free space is just k1 , we can start P1 again so that the whole space is totally occupied.4. When , n is an integer, one process is just being finished, we can start another process.It is shown in this paper that the time-space efficiency rate of this algorithm is also .