| The model of simple batch systems is the research foundation of its performance evaluation, simulation, scheduling and control. From the existing literature, the model of simple batch systems mainly use timed automata, timed petri nets and timed extension of process algebra while timed automata and timed petri nets have extensive influence and application.This paper introduces a mathematical model named batch automata for simple batch systems, which is a meaningful attempt for modeling and verifying the simple batch systems, even operation systems. Compared with timed automata and timed petri nets, the model is useful to modeling for simple batch systems.Timed control matrix is led when setting up a model, which can compute, save the respond ratio of progresses in various scheduling algorithms. It is general used and simple calculation. The author translates the model into the Kripke structure, codes the state from multi value to boolean value, and gives the corresponding algorithm. Then, it's easy to describe the system property by boolean logic. Combined with an example, the paper verifies the simple batch systems based on the Kripke structure and CTL. And the result shows that it is correct to compute the respond ration of progresses by using timed control matrix. The model built in the paper is reasonable. Moreover, using the fix point in the process makes the algorithm simpler and its automation higher.Finally the author converts the model into Buchi automata, combining with the automata theory gives another model checking algorithm, proves the rationality of the algorithm, and implements the programming with code. |
