Timed Automata with Asynchronous Processes: Schedulability and Decidability
(Joint work with Tobias Amnell, Elena Fersman, Paul Pettersson)
We adopt a model of timed automata extended with asynchronous processes
i.e. tasks triggered by events. A task is an executable program
characterized by its worst execution time and deadline, and possibly other parameters such
priorities etc. for scheduling. The main idea is to associate each
location of an automaton with a set of tasks. A transition leading to a
location in the automaton denotes an event triggering the tasks and the clock
constraint on the transition specifies the possible arrival times of the event.
This yields a general task model for real-time systems in which tasks may be
periodic and non-periodic. An automaton is schedulable if there exists
a scheduling strategy such that all possible sequences of events accepted by
the automaton are schedulable in the sense that all associated tasks can be
computed within their deadlines.
Our main result is that the schedulablity checking problem
for extended automata is decidable. The proof is based on a variant of
timed automata, that is timed automata with subtraction in which clocks
may be updated by subtraction. We show that if each clock is bounded with
a maximal constant and subtraction operations are performed on clocks only
the bounded zone, the reachability problem is decidable. The crucial
observation is that subtraction preserves region equivalence
in the bounded clock zone, and the schedulability checking problem can
be translated to a reachability problem for bounded timed automata
with subtraction. Based on the proof, we have developed a symbolic
technique for schedulability analysis for timed systems, which has
been implemented as a prototype model checker in UPPAAL.
Place: Information technology, Uppsala University
Time: 13.15-14.00 (the seminar will continue with Tobias Amnells seminar)
Room 1113 is in building 1, floor 1, room 13
(in the southern part of the building).
Help on how to find ASTEC Seminars.
Everyone is welcome !
Updated 23-Oct-2001 09:27 by Roland Grönroos
e-mail: info -at- astec.uu.se