Abstract
We study a methodology for constructing scheduled systems by restricting successively the behavior of the processes to be scheduled. Restriction is used to guarantee the satisfaction of two types of constraints: schedulability constraints characterizing timing properties of the processes, and constraints characterizing particular scheduling algorithms including process priorities, non-idling, and preemption.
The methodology is based on a controller synthesis paradigm. The main results deal with the characterization of scheduling policies as safety constraints and the simplification of the synthesis process by applying a composability principle.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
K. Altisen, G. Gößler, A. Pnueli, J. Sifakis, S. Tripakis, and S. Yovine. A framework for scheduler synthesis. In IEEE RTSS 1999 proceedings, 1999.
S. Bornot, G. Gößler, and J. Sifakis. On the construction of live timed systems. In TACAS 2000, volume 1785 of LNCS. Springer-Verlag, 2000.
S. Bornot and J. Sifakis. On the composition of hybrid systems. In International NATO School on “Verification of Digital and Hybrid Systems”, LNCS. Springer Verlag, 1997.
P.A. Hsiung, F. Wang, and Y.S. Kuo. Scheduling system verification. In TACAS’99, volume 1597 of LNCS. Springer-Verlag, 1999.
Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine. Integration graphs: A class of decidable hybrid systems. Information and Computation, 736, 1992.
H.-H. Kwak, I. Lee, A. Philippou, J.-Y. Choi, and O. Sokolsky. Symbolic schedulability analysis of real-time systems. In IEEE RTSS 1998 proceedings, 1998.
C.L. Liu and J.W. Layland. Scheduling algorithms for multiprogramming in a hard-real-time environment. Journal of the ACM, 20(1), 1973.
Z. Liu and M. Joseph. Specification and verification of fault-tolerance, timing, and scheduling. ACM Transactions on Programming Languages and Systems, 21(1):46–89, 1999.
O. Maler, A. Pnueli, and J. Sifakis. On the synthesis of discrete controllers for timed systems. In STACS’95, volume 900 of LNCS. Springer Verlag, 1995.
P. Niebert and S. Yovine. Computing optimal operation schemes for chemical plants in multi-batch mode. In Hybrid Systems, Computation and Control, volume 1790 of LNCS. Springer Verlag, 2000.
P.J. Ramadge and W.M. Wonham. Supervisory control of a class of discrete event systems. Journal of Control and Optimization, 25(1), 1987.
L. Sha, R. Rajkumar, and J. P. Lehoczky. Priority inheritance protocols: An approach to real-time synchronization. IEEE Transactions on Computers, 39(9), 1990.
S. Vestal. Modeling and veri_cation of real-time software using extended linear hybrid automata. In Fifth NASA Langley Formal Methods Workshop, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Altisen, K., Gößler, G., Sifakis, J. (2000). A Methodology for the Construction of Scheduled Systems. In: Joseph, M. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 2000. Lecture Notes in Computer Science, vol 1926. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45352-0_11
Download citation
DOI: https://doi.org/10.1007/3-540-45352-0_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41055-3
Online ISBN: 978-3-540-45352-9
eBook Packages: Springer Book Archive