In this paper, we exend timed automata with asynchronous processes
i.e. tasks triggered by events as a model for real-time systems. The
model is expressive enough to describe concurrency and
synchronization, and real time tasks which may be periodic, sporadic,
preemptive and (or) non-preemptive. We generalize the classic notion
of schedulability in scheduling theory to timed au- tomata as
follows. An automaton is schedulable if there exists a (preemptive or
non-preemptive) scheduling strategy such that all possible sequences
of events ac- cepted by the automaton are schedulable in the sense
that all associated tasks can be computed within their deadlines. Our
main result is that the schedula- bility checking problem is decidable
To our knowledge, this is the rst general decidability result on
automata-theoretic models for real time scheduling without assuming
that preemptions occur only at integer time points. The proof is based
on a class of updatable automata: timed automata with subtraction in
which clocks may be updated by subtractions. We show that if each
clock is bounded with a maximal constant and subtraction operations
are performed on clocks only in the bounded zone, the reachability
problem is decidable. The crucial observa- tion is that the
schedulability checking problem can be encoded as a reachability
problem for such automata using clock subtractions. Based on the
proof, we have developed a symbolic technique, which has been
implemented as a prototype tool for schedulability analysis.