● 摘要
单道批处理系统的模型是其性能评价、仿真、作业调度及控制的研究基础. 已有文献中,单道批处理系统的建模主要使用了时间自动机, 时间Petri网, 以及进程代数的时间扩充等各种方法, 其中以时间自动机与时间Petri网的影响和应用最为广泛.
本文为单道批处理系统建立了一个新数学模型, 即批处理自动机, 该模型是批处理系统乃至操作系统建模与验证的一个有意义的尝试. 与时间自动机和时间Petri网相比, 利用批处理自动机对简单批处理系统建模具有更强的适用性.
建模时引入时序控制矩阵, 可计算、存储各种调度算法下作业响应比; 通用性强, 计算简单, 自动化程度高. 作者将所建模型转化成Kripke结构, 将节点状态值由多值编码成二值的, 给出了相应的转换算法; 便于用二值逻辑公式描述系统性质.
结合实例进行了基于Kripke结构和线性计算树逻辑的简单批处理系统形式化验证, 结果表明利用时序控制矩阵计算存储作业响应比的算法是正确的; 本文所建批处理自动机模型是合理的; 验证过程所用不动点计算算法简单且自动化程度较高.
将模型最终转化为Büchi自动机, 结合自动机理论给出了另一种模型检测方法, 证明了算法的合理性; 并用代码实现了该算法.
相关内容
相关标签