Schedulability Analysis for Distributed Systems Using Network of Action Automata and Environment Automata

Recently, several formal approaches have been presented to address the problem of schedulability analysis of real-time systems by some varieties of timed automata, e.g., UPPAAL and TIMES. In this paper, we consider a more general and complicated formal computational model for distributed systems. To analyze the schedulability of tasks within this model by automata theory, we present a model, action automata, which is a class of suspension automata, to describe the execution semantics of tasks, we also define an environment model, environment automata, to describe the arrival patterns of tasks. One main result gives the scheduling policies under which the schedulability can be analyzed by our method correctly. To achieve this result, we translate the schedulability analysis to the reach ability analysis of the network of action automata and environment automata. Therefore, another main result of this paper is that we prove the reach ability of action automata is decidable. Based on these conclusions, we implement a prototype tool for schedulability analysis and test its performance under EDF policy.