单道批处理系统的建模与验证  

Modeling and Verification of Batch System

作　　者：鱼先锋[1] 雷丽晖[1] 李永明[1] 

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

出　　处：《计算机科学》2011年第4期257-259,共3页Computer Science

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

摘　　要：单道批处理系统的模型是其性能评价、仿真、作业调度及控制的研究基础。建立了单道批处理系统的一个数学模型——批处理自动机,并给出了相应的转换算法,将所建数学模型转换成Kripke结构;完成了基于Kripke结构的单道批处理系统模型检测,验证了单道批处理系统的合理性即兼顾公平性与效率。The model of simple batch systems is the foundation of its performance evaluation,simulation,scheduling,and control research.This paper introduced a mathematical model named batch automata for simple batch systems,and gave an algorithm for translating a batch automata into a Kripke structure,and completed the model checking of batch system based on the Kripke structure to verify the reasonable property,i.e.,both fair and efficiency.

关 键 词：批处理系统 模型检测 KRIPKE结构 自动机 

分 类 号：TP316[自动化与计算机技术—计算机软件与理论]