General model of real-time modular computer systems operation for checking acceptability of such systems configurations

In this paper, we consider schedulability analysis problem for real-time modular computer systems (RT MCS). A system configuration is called schedulable if all the jobs complete within their deadlines. The paper contains formal definitions of a system configuration and a system operation trace which is necessary for checking the schedulability criterion. The author proposes a stopwatch automata-based general model of RT MCS operation. A model instance for a given RT MCS configuration is a network of stopwatch automata and it can be built automatically using the general model. A system operation trace can be obtained from the corresponding NSA trace. The stopwatch automata formalism allowed us to prove that the model is deterministic and satisfies a set of correctness requirements derived from RT MCS specifications. We implemented our approach in software and compared it experimentally with Model Checking approach, which uses the same formalism. The results of the experiments confirm that our approach is much more efficient. The software implementation is also integrated with the existing industrial RT MCS scheduling tool. These experiments showed the applicability of the proposed approach to real scale systems.