Abstract
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 as 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 in 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.

ASTEC seminar
October 30, 2001

Place: Information technology, Uppsala University
Room: 1113
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.