Font Size: a A A

Research On The Formalized Description Method Of Mobile Communication System

Posted on:2020-12-08Degree:DoctorType:Dissertation
Country:ChinaCandidate:H BuFull Text:PDF
GTID:1368330620952210Subject:Communication and Information System
Abstract/Summary:PDF Full Text Request
Presently,various countries pay more and more attention on the construction of the ground-air-space network information system(GASNIS),which consists of the aerial platform(such as the space station,the satellite of low,middle and high orbits,the stratospheric balloon,the manned or unmanned aircraft),the ground platform(such as the ground station or the ground mobile terminal)and the water platform(such carrier as the ocean observing ship or other ships with special missions).Thus,GASNIS is a network information system mainly responsible for the real-time access,transmission and relevant information process,its development concerning many important domains like national politics,economy,military matters and people’s livelihood.As a complex system,GASNIS itself has constantly changing topological structures,while the tasks requirement made by the user may be complicated and varied,leading to the concurrent movements of too many user processes in a topologically structured changing system.Moreover,its transmission rate may also be influenced by the physical environment in the space or on the ground,increasing the even more complexity of the system.Therefore,in order to make use of the system resources and improve the service quality of the system,we need to carry on the reasonable dispatching to all the tasks in GASNIS.The problems of task dispatching mainly focus on the execution sequence of the tasks and the qualitative and quantitative analysis on the tasks and limited resources for the realization of their highly effective coupling.The nature in the execution sequence of the tasks is sorting them out according to their weights,while the nature of the qualitative and quantitative analysis on the tasks and resources,actually is the space-time analysis for the task on the quality and quantity of its resource demands and resource supplies in the environment of the system,on the basis of clear definition and description of the dispatching subjects and environment.In order to achieve better dispatching of GASNIS tasks,i.e.to improve the responding speed and reasonableness of dispatching,two studies need to be done well:firstly,the sequencing algorithm adapted to the concurrent environment needs to be studied to improve the responding speed of sorting;secondly,the proper tool must be studied to describe the dispatching of GASNIS tasks,on the basis of which to analyze and verify the task dispatching in the system.To deal with the first problem: the dissertation has proposed various kinds of algorithms for concurrent sorting to handle the task sorting problem according to the task weight when task dispatching is needed.According to different storage methods,two sorting algorithms are proposed in the dissertation: one is the concurrent sorting based on elements stored by linked lists for dealing with elements stored in linked lists,while the other is the concurrent sorting algorithm based on elements stored by index for dealing with elements stored by index.In the sorting algorithm of elements stored in linked lists,the conventional algorithm has relatively low efficiency.The dissertation takes the features of concurrency into account to propose the sorting algorithm for the elements in the linked-list-based storage,in which m elements are sorted out for a sequence in a linked list with the length of n,so that the element comparison could be done at most for 2n-m times.In sorting elements based on indexed storage,the dissertation has first proposed the filtering sorting algorithm,on which basis three more algorithms are proposed in combination of the idea of concurrency---the concurrent filtering sorting algorithm and the sorting algorithm with concurrent filtering insertion.The concurrent filtering sorting requires the least time when there are enough resources,especially when there are enough corresponding hardware supports.Suppose the required time for the comparison of two elements is t1,and the total time for the concurrency of 1 for n times,then no matter how many elements there are,theoretically,the required time for sorting will be t1+t2 when the concurrency rate reaches 100%.On the other hand,the sorting with concurrent filtering insertion takes relatively more time and fewer resources.In order to apply these algorithms directly to the task dispatching of GASNIS,the dissertation has made the formalized description,reasoning and verification for them.It is hence found that these concurrent sorting algorithms are adaptable not only to the task dispatching of GASNIS,but also to other computing environments where the sorting function is needed.To deal with the second problem: the dissertation has made syntactic and semantic extension from the perspective of quantitative description on the base of seal calculus,forming the quantification of seal calculus.The detailed extension is as follows:1)As to the problem of lacking the quantitative description of the process and seal,the dissertation has proposed the idea of resource quantification,which means the quantitative extension of seal labels and process names in describing.Among them,the meaning of a seal label has changed from merely a domain name to an ordered pair which is combined with both a name and resource supply function matrix.On the other hand,the meaning of process names has changed from merely a name to an ordered pair which is combined with both a name and the resource demand function matrix.Only in this way could GASNIS be analyzed and investigated from the perspective of the resource supplies in seal and resource demands in processes,so as to make up for the inability to make quantitative description of the seal calculus.2)As to the locational problem of the process operation,the dissertation has creatively proposed the idea of locational quantification,that is,the locational description of processes in more specific details.Firstly,the meaning of the "movement" has been expanded in the seal calculus by making the rule of allowing processes to move,in order to solve the problem of inability to move the seal for simulation in the real system,especially when part of processes are needed to move in the system.Secondly,to deal with the problem of binding some particular resource in a specific position,a new rule is proposed to allow the locking and unlocking of the process location,in order to solve the security problem in the process classification and the matching between some specific process and resource after the classification.That is,the locked process could not move randomly unless it is unlocked by the dispatching system.Thirdly,to deal with the chaos caused by the internal processes of the moved seal and locational superscript indicators related to the process of the seal,a revising rule is proposed in the superscript location of the process,improving the flexibility of the seal movement with wider application.3)To deal with the problem of unlimited uses of resources probably caused by duplicated operators,the dissertation has proposed the idea of concurrence and duplication quantification,by making the constraint rule for unlimitedly duplicated operators,increasing the superscripts of unlimitedly duplicated operators to limit the maximum number of process concurrency,and allowing the superscript revision of unlimitedly duplicated operators to adapt to the resource changes in seal.In this way,the description of the resource uses and control is realized for improving the usage rate of resources and executing efficiency of the system.4)To deal with the lack of description in the intermediate state of processes which in turns causes the lack of detection and control over the system resources in dispatching,the dissertation has proposed the idea of process quantification,by extending the meaning of τ,which is used to symbolize the internal actions or the intermediate state of related process operation,so that the description problem could be solved for the processes in the intermediate state of dispatching.The introduction of the intermediate state of the process operation also means the introduction of the description in time control,which matters a lot in the analysis of task dispatching.The interrupt description can make the quantification of seal calculus better and more comprehensive to describe the system.The application of the quantification of seal calculus to the system description will be of great help for us,in the early designing period to find out the inconsistency,incompletion,ambiguity as well as other logic errors of the system;in the middle designing period to build a simple but simulated system for the simulation of the dynamic system when a large number of tasks come in and out of the resources,and to verify the concurrent movement and execution of many more processes in the dynamically changing node groups;in the later designing period to facilitate the analysis and estimation of the system efficacy,and trace the system flaws,so that the error analysis,maintenance and evaluation of the system could be done well.The dissertation is ended with the summary of researches in the formalized description of the mobile communication system,posing the future research questions on further quantification,schematized description and the modeling of the framework in the formalized description etc.
Keywords/Search Tags:the ground-air-space network information system, concurrent sorting in linked-list-based storage, concurrent filtering sorting, sorting with concurrent filtering insertion, quantification of seal calculus
PDF Full Text Request
Related items