关键词: 多处理器调度算法，线性时序逻辑，模型检测，扩展I3iichi自动机

Abstract: In multiprocessor systems, the tasks which need to be completed by an application can be distributed onto the same processor or a group of processors. Therefore, software testing is unable to verify the reliability of multiprocessor scheduling algorithms. Thus a formal model based on extended I3iichi automata which is used to describe the丁DS CTask Duplication based Scheduling) algorithm was presented. I}he expected properties of the algorithm were described by 1i near temporal logic formulas and verified on the above model. This method overcomes the limitations of software testing and can be used to check the reliability of the multiprocessor task scheduling I’DS.

Key words: Multiprocessor scheduling algorithm, Linear temporal logic, Model checking, Extended biichi automata