Modeling and Verification of Batch System
单道批处理系统的建模与验证

单道批处理系统的模型是其性能评价、仿真、作业调度及控制的研究基础。建立了单道批处理系统的一个数学模型—批处理自动机，并给出了相应的转换算法，将所建数学模型转换成Kripke结构;完成了基于Kripke结构的单道批处理系统模型检测，验证了单道批处理系统的合理性即兼顾公平性与效率。