多处理器任务调度算法TDS的建模与验证  

Modeling and Verifying Scheduling Algorithm TDS for Multiprocessor Systems

作　　者：李召妮[1] 雷丽晖[1] 李永明[1] 

机构地区：[1]陕西师范大学计算机科学学院,西安710062

出　　处：《计算机科学》2012年第11期301-304,F0003,共5页Computer Science

基　　金：国家自然科学基金(60873119;61003061);高校博士学科点专项科研基金(20090202120006);中央高校基本科研业务费(GK200902017;GK201001003)资助

摘　　要：在多处理器系统中,一个应用所要完成的任务可以分配给同一个处理器处理,也可以分配给多个处理器处理,所以传统的测试方法难以满足多处理器任务调度算法的验证。在此,提出一个基于扩展Büchi自动机的形式化模型,并用该模型来描述多处理器任务调度算法TDS(Task Duplication based Scheduling);用线性时序逻辑描述出算法TDS期望的一些性质;最后在该模型上验证了这些性质。该方法有效地克服了传统测试的局限性,保证了多处理器任务调度的可靠性。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 Büchi automata which is used to describe the TDS（Task Duplication based Scheduling） algorithm was presented.The expected properties of the algorithm were described by li-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 TDS.

关 键 词：多处理器调度算法 线性时序逻辑 模型检测 扩展Büchi自动机 

分 类 号：TP301.1[自动化与计算机技术—计算机系统结构]