计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2012年
11期
301-304,封3
,共5页
多处理器调度算法%线性时序逻辑%模型检测%扩展Büchi自动机
多處理器調度算法%線性時序邏輯%模型檢測%擴展Büchi自動機
다처리기조도산법%선성시서라집%모형검측%확전Büchi자동궤
在多处理器系统中,一个应用所要完成的任务可以分配给同一个处理器处理,也可以分配给多个处理器处理,所以传统的测试方法难以满足多处理器任务调度算法的验证.在此,提出一个基于扩展Büchi自动机的形式化模型,并用该模型来描述多处理器任务调度算法TDS(Task Duplication based Scheduling)；用线性时序逻辑描述出算法TDS期望的一些性质；最后在该模型上验证了这些性质.该方法有效地克服了传统测试的局限性,保证了多处理器任务调度的可靠性.
在多處理器繫統中,一箇應用所要完成的任務可以分配給同一箇處理器處理,也可以分配給多箇處理器處理,所以傳統的測試方法難以滿足多處理器任務調度算法的驗證.在此,提齣一箇基于擴展Büchi自動機的形式化模型,併用該模型來描述多處理器任務調度算法TDS(Task Duplication based Scheduling)；用線性時序邏輯描述齣算法TDS期望的一些性質；最後在該模型上驗證瞭這些性質.該方法有效地剋服瞭傳統測試的跼限性,保證瞭多處理器任務調度的可靠性.
재다처리기계통중,일개응용소요완성적임무가이분배급동일개처리기처리,야가이분배급다개처리기처리,소이전통적측시방법난이만족다처리기임무조도산법적험증.재차,제출일개기우확전Büchi자동궤적형식화모형,병용해모형래묘술다처리기임무조도산법TDS(Task Duplication based Scheduling)；용선성시서라집묘술출산법TDS기망적일사성질；최후재해모형상험증료저사성질.해방법유효지극복료전통측시적국한성,보증료다처리기임무조도적가고성.
