Formalization Of The Parallel Real-time System In BRCC

Extended real-time systems and spatial reasoning are two emerging areas of current scientific and technological research, both play an important role in the theory and engineering application. Real-time system is mainly of a given constrained multi-task scheduling arrangements, and these tasks have deadlines . DDS (Deadline-Driven Scheduler, the deadline priority scheduling method) is able to handle scheduling problems nicely under a single-processor; but to deal with multi-processor environment, the study on global scheduling is still at its prelimilary stage in recent years, PFair ( Proportional fair ) method proposed by Baruah is a typical global scheduling technique. On the other hand, the spatial reasoning provide useful formal tools for modeling of spatial objects, spatial knowledge representation, spatial relations representation and reasoning etc. Among various frmal systems of spatial Logic, RCC (Region Connection Calculus) is the most advantageous and most convenient logical system that deals with characterization and reasoning of spatial relations. Düntsch, Li Sanjiang and others have shown that the semantic of BRCC system is mainly the models that contain an Boolean algebra and a binary relation C(x, y), known as relational algebras or connected Boolean algebras.The subject proposed by us independently in this paper is just in the intersection of these two areas. After the brief representation of background and current development of international research society in the areas, we will discusse in detail the problems of formaling parallel scheduling and CBA semantic (Contact Boolean Algebra), then we will propose an extended BRCC language and axiom system in order to achieve a formal characterization of the parallel scheduling, and intensively study the formal inference of the effectiveness of the parallel scheduling and existence of optimal scheduling. Among them, modular CBA semantic and its nature are the key points. Our main results are listed as following:⑴For a class of extended real-time systems, we have designed two simple decision-algorithms for the existence of effective scheduling: the enhanced simplex method and the enhanced greedy algorithm.⑵By using the"time slice"technology in engineering application, we have proposed a method for discretization of real-valued data-type. CBA models of scheduling programs have been constructed .⑶Based on the CBA models construced in (2) , we have extened the BRCC language, a formalization of scheduling programs is presented .This article is organized as follows:Chapter 1 The relevant historical background and significance of this studyChapter 2 The extended model of parallel real-time systemChapter 3 Extended real-time systems can be determined, giving two decision algorithms: modified simplex method and the enhanced greedy algorithm.Chapter 4 Introduction of the spatial logic and BRCC system.Chapter 5 After the introduction of Boolean algebra, parallel real-time systems are given semantic model of CBAChapter 6 Extending BRCC language and formalizing schedulingChapter 7 Summary and Outlook...