Research On Analysis And Optimization Of Task Scheduling Systems Of Distributed Integrated Modular Avionics

With the rapid technological advance in micro-processors and high-speed networks,there is a growing trend towards airborne resource sharing,data fusion and mission synthesis in the aviation industry.For this purpose,the new generation of avionics systems,Distributed Integrated Modular Avionics(DIMA),adopts the generalized distributed computing architecture that suits the requirement of safe-critical applications in avionics systems.However,the development of the task scheduling system of DIMA faces serious challenges of its high system complexity,various real-time task behavior,heavy workload,etc.The traditional approaches to analysis and optimization of real-time systems have not been applicable to the analysis or development in DIMA architecture due to their insufficient expressiveness,conservative schedulability conditions and waste of processor time.Therefore,it is necessary to build a novel methodology of DIMA task scheduling that meets the aviation standards and the requirements of complex avionics applications.This thesis focuses on the analysis and optimization of task scheduling systems of DIMA,which are divided into four major problems: system modeling,schedulability analysis,generation of schedules and allocation of processor resource.We undertake the corresponding research on formal modeling of DIMA systems,compositional schedulability verification,automatic generation of schedules,and optimization of scheduling systems.The main innovative work of this thesis is as follows:1.To support the modeling of task scheduling systems of DIMA,this thesis defines the syntax and semantics of an extended stopwatch automata,which introduces a set of channel-based intermodel communication rules and adopts stochastic semantics to describe the non-deterministic delay in DIMA systems.By using the extended stopwatch automata,we build the formal model of task scheduling systems of DIMA.The model covers the major temporal behavioral features of DIMA architecture,such as partition scheduling mechanism,multi-core processors,intertask/-partition dependency,multiple types of task behavior,communication via avionics networks,etc,realizing a precise description of the distributed structure and global communication of DIMA.The model is compatible with both symbolic and statistic model checking(SMC).By using the SMC simulation-based tests,we can fast falsify non-schedulable schemes,thus reducing the computational cost of schedulability analysis.The thesis designs conformance test cases based on timed computation tree logic,which verify the standardized temporal features of DIMA architecture including isolation between partitions,periodicity of partition scheduling,preemptive scheduling of real-time tasks,and connectivity of virtual links.Compared with the existing modeling work,the model presented in this thesis is not only more expressive but also efficient at analyzing schedulability.2.Owing to the high system complexity,various real-time tasks,heavy workload of DIMA systems,the classic model checking of DIMA formal models is confronted with the statespace explosion problem,which makes it impossible to apply classic model checking to the schedulability analysis of DIMA systems.The earlier techniques of compositional verification are promising to mitigate the state-space explosion,but they did not consider the underlying network communication between avionics partitions,thus rendering them inapplicable to DIMA systems.This thesis proposes a compositional approach to schedulability verification of DIMA systems,which constructs compositional reasoning rules on the basis of assumeguarantee paradigm and defines a message interface model that describes the communications between partitions.The approach checks each partition individually on a small scale and then assembles the local results together to derive conclusions about the schedulability of an entire system.In doing so,the result of each partition is based on the assumptions of its communication environment while the real environment also guarantees the assumptions,which ensures the correctness of global conclusion.Compared with the existing compositional methods,the approach presented in this thesis is able to cope with the dependency between partitions and to perform more precise schedulability analysis by considering the effect of distributed architecture and network communication in DIMA systems.3.This thesis designs a parameter-sweep based method for automatic generation of the schedules in DIMA systems,implementing the generation of partition schedules as a Parameter Sweep Application(PSA)that performs a heuristic search of the parameter space of partition resource models.The PSA creates a formal model for each candidate parameter combination and undertakes parallel heuristic exploration of the formal models in the parameter space to find schedulable partition resource models.According to the balance between hierarchical demand and supply,a generation algorithm converts the partition resource model obtained from the parameter sweep into a partition schedule.By constructing the testing structure of timed selection simulation,we define a test automaton for the extended stopwatch automata.The method realizes an automatic schedulability analysis,where the test automaton is introduced to verify the abstraction-refinement relations between partitions and their message interfaces in the parameter sweep process.The experiment shows that our method not only achieves the automatic design of partition schedules but also improves processor utilization due to the application of more expressive formal models.4.Traditional optimization methods require the analytical expressions of constraints and objective function,but complex avionics system models lack precise analytical descriptions.As a result,traditional optimization methods cannot handle the avionics properties and behaviors in formal models directly.This thesis proposes an evolutionary-computing based method for optimizing the task scheduling systems of DIMA,integrating the above automatic schedulability analysis based on stopwatch automata into the framework of evolutionary computing,where the fitness value of each individual is evaluated by combining the schedulability satisfaction and processor occupancy.To improve the search efficiency and adaptability of the evolutionary algorithm,we design the evolution operators including local line recombination and rotated Gaussian mutation and define a set of strategy parameters to control the search directions and mutation strength of the evolution operators.The self-adaptation of these strategy parameters is achieved via on-policy reinforcement learning.The optimization experiment demonstrates that the method is able to acquire the processor resource allocation with low workload and meanwhile avoids exhaustive search and premature convergence.