A formal framework is proposed for the verification of complex
real-time systems, modeled as client-server scheduling systems,
using the popular model-checking approach. Model-checking is
often restricted by the large state-space of complex real-time
systems. The scheduling of tasks in such systems can be taken
advantage of for model-checking. Our implementation and
experiments corroborate the feasibility of such an approach.
Wide-applicability, significant state-space reduction, and several
scheduling semantics are some of the important features in our theory
and implementation.
Keywords
scheduling algorithms, model-checking, timed automata,
client-server systems