zbMATH — the first resource for mathematics

Task automata: Schedulability, decidability and undecidability. (English) Zbl 1121.68062
Summary: We present a model, task automata, for real time systems with non-uniformly recurring computation tasks. It is an extended version of timed automata with asynchronous processes that are computation tasks generated (or triggered) by timed events. Compared with classical task models for real time systems, task automata may be used to describe tasks (1) that are generated non-deterministically according to timing constraints in timed automata, (2) that may have interval execution times representing the best case and the worst case execution times, and (3) whose completion times may influence the releases of task instances. We generalize the classical notion of schedulability to task automata. A task automaton is schedulable if there exists a scheduling strategy such that all possible sequences of events generated by the automaton are schedulable in the sense that all associated tasks can be computed within their deadlines. Our first technical result is that the schedulability for a given scheduling strategy can be checked algorithmically for the class of task automata when the best case and the worst case execution times of tasks are equal. The proof is based on a decidable class of suspension automata: timed automata with bounded subtraction in which clocks may be updated by subtractions within a bounded zone. We also study the borderline between decidable and undecidable cases. Our second technical result shows that the schedulability checking problem will be undecidable if the following three conditions hold: (1) the execution times of tasks are intervals, (2) the precise finishing time of a task instance may influence new task releases, and (3) a task is allowed to preempt another running task.

68Q45 Formal languages and automata
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI
[1] Buttazzo, G.C., Hard real-time computing systems. predictable scheduling algorithms and applications, (1997), Kluwer Academic Publishers · Zbl 0890.68016
[2] Ericsson, C.; Wall, A.; Yi, W., Timed automata as task models for event-driven systems, ()
[3] McManis, J.; Varaiya, P., Suspension automata: a decidable class of hybrid automata, (), 105-117
[4] Larsen, K.G.; Pettersson, P.; Yi, W., Compositional and symbolic model-checking of real-time systems, (), 76-89
[5] Alur, R.; Dill, D.L., A theory of timed automata, Theoretical computer science, 126, 2, 183-235, (1994) · Zbl 0803.68071
[6] Bengtsson, J.; Yi, W., Timed automata: semantics, algorithms and tools, () · Zbl 1088.68119
[7] Henzinger, T.; Kopke, P.; Puri, A.; Varaiya, P., What’s decidable about hybrid automata?, Journal of computer and system sciences, 57, 94-124, (1998) · Zbl 0920.68091
[8] Fersman, E.; Pettersson, P.; Yi, W., Timed automata with asynchronous processes: schedulability and decidability, (), 67-82 · Zbl 1043.68589
[9] Krčál, P.; Yi, W., Decidable and undecidable problems in schedulability analysis using timed automata, (), 236-250 · Zbl 1126.68456
[10] Amnell, T.; Fersman, E.; Mokrushin, L.; Pettersson, P.; Yi, W., TIMES—a tool for modelling and implementation of embedded systems, () · Zbl 1043.68513
[11] Fersman, E.; Mokrushin, L.; Pettersson, P.; Yi, W., Schedulability analysis of fixed-priority systems using timed automata, Theoretical computer science, 354, 2, 301-317, (2006) · Zbl 1088.68087
[12] Altisen, K.; Gößler, G.; Pnueli, A.; Sifakis, J.; Tripakis, S.; Yovine, S., A framework for scheduler synthesis, (), 154-163
[13] Altisen, K.; Gößler, G.; Sifakis, J., A methodology for the construction of scheduled systems, (), 106-120 · Zbl 0986.90501
[14] Abdeddaim, Y.; Maler, O., Job-shop scheduling using timed automata, () · Zbl 0991.68507
[15] Fehnker, A., Scheduling a steel plant with timed automata, ()
[16] Hune, T.; Larsen, K.G.; Pettersson, P., Guided synthesis of control programs using U{\scppaal}, Nordic journal of computing, 8, 1, 43-64, (2001) · Zbl 0978.68021
[17] Corbett, J., Modeling and analysis of real-time ada tasking programs, (), 132-141
[18] Cassez, F.; Laroussinie, F., Model-checking for hybrid systems by quotienting and constraints solving, (), 373-388 · Zbl 0974.68117
[19] Alur, R.; Courcoubetis, C.; Halbwachs, N.; Henzinger, T.A.; Ho, P.-H.; Nicollin, X.; Olivero, A.; Sifakis, J.; Yovine, S., The algorithmic analysis of hybrid systems, Theoretical computer science, 138, 1, 3-34, (1995) · Zbl 0874.68206
[20] Bouyer, P.; Dufourd, C.; Fleury, E.; Petit, A., Are timed automata updatable?, () · Zbl 0996.68121
[21] Larsen, K.G.; Yi, W., Time-abstracted bisimulation: implicit specifications and decidability, Information and computation, 134, 2, 75-101, (1997) · Zbl 0887.68068
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.