Verification Of Deterministic Scheduling Algorithm For Heterogeneous Processors

The increasing demand for strong real-time and high-reliability requirements in safety-critical embedded systems has led to the adoption of heterogeneous computing platforms to provide high-performance computing support as an important feature and trend of the next-generation embedded systems.The resource partitioning method,task scheduling algorithm,and runtime system control mechanism directly affect the system resource utilization and real-time response capability.Real-time task scheduling planning directly affects the correctness of system behavior,and efficient scheduling algorithms and reliable verification methods are crucial to ensuring the safe and orderly execution of safety-critical system tasks.This thesis proposes a time-deterministic scheduling algorithm and a formal verification method for heterogeneous computing platform real-time reliability issues.Firstly,a periodic segmented task scheduling algorithm for heterogeneous computing platforms is proposed.At the same time,a formal verification framework is constructed for this algorithm,and the correctness of the algorithm is proved.The main research contents are as follows:(1)For heterogeneous computing platforms and periodic segmented task models,the linear constraints that time-deterministic scheduling needs to satisfy are studied,and the performance differences of algorithms under different optimization objectives are analyzed.A time-deterministic scheduling algorithm that maximizes the execution window is proposed as the optimization objective.(2)Based on software formal methods,a layered verification framework for heterogeneous time-deterministic scheduling algorithms is constructed,forming a model layer,a constraint layer,and a verification layer analysis architecture.For the real-time task scheduling characteristics of the heterogeneous computing platform,a formal model for real-time scheduling of the heterogeneous computing platform is constructed at the model layer,which decomposes the real-time scheduling of the heterogeneous computing platform into five basic modules,including the time module,processor module,task module,arrival sequence module,and scheduling module.The five modules describe the core concepts related to real-time scheduling of heterogeneous computing platforms and serve as the basis for formal specifications and formal verification.(3)The constraint layer establishes a formal specification for time-deterministic scheduling,models and refines the linear programming constraints,and uses them as the premise assumptions for theorem proving in the verification layer.Based on the characteristics of the heterogeneous computing platform real-time task scheduling algorithm,six correctness theorems that this algorithm needs to satisfy are proposed from the aspects of real-time performance and functional correctness.The interactive theorem prover Coq is used to describe the propositions and logic systems of the theorems to be proven.(4)Based on the Coq proof tool and the SSReflect proof strategy library,a theorem proving method is used to formally verify the six theorems in the verification layer,ensuring the correctness of the time-deterministic scheduling algorithm proposed in this thesis.