Abstract
This paper shows how the feasibility of scheduling a realtime program consisting of a number of parallel processes (tasks) can be proved as a step in the refinement of the program from its specification. Verification of this step of refinement makes formal use of methods and results from real-time scheduling theory.
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
M. Abadi and L. Lamport. The existence of refinement mapping. In Proc. 3rd IEEE Symposium on Logic and Computer Science, 1988.
M. Abadi and L. Lamport. An old-fashioned recipe for real-time. In W.P. de Rover J.W. de Bakker, C. Huizing and G. Rozenberg, editors, Real-Time: Theory in Practice, Lecture Notes in Computer Science 600. Springer-Verlag, 1992.
A. Burns, R. Davis, and S. Punnekkat. Feasibility analysis of fault-tolerant real-time tasks. Technical report, Department of Computer Science, University of York, 1995.
A. Burns and A. Wellings. Advanced fixed priority scheduling. In M. Joseph, editor, Real-Time Systems: Specification, Verification and and Analysis, pages 32–65. Prentice Hall, 1996.
T. Henzinger, Z. Manna, and A. Pnueli. Temporal proof methodologies for real-time systems. In Proceedings of the 8th ACM Annual Symposium on Principles of Programming Languages, pages 269–276, 1991.
L. Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, 1994.
Z. Liu and M. Joseph. Specifying and verifying of recovery in asynchronous communicating systems. In J. Vytopil, editor, Formal Techniques in RealTime and Fault Tolerant Systems, pages 137–166. Kluwer Academic Publishers, 1993.
Z. Liu and M. Joseph. Formalizing real-time scheduling as program refinement. Technical report, Department of Maths and Computer Science, University of Leicester, 1996.
Z. Liu and M. Joseph. Verification of fault-tolerance and real-time. In Proceedings of the 26th Annual International Symposium on Fault-Tolerant Computing, pages 220–229. IEEE Computer Society, 1996.
Z. Liu, M. Joseph, and T. Janowski. Verification of schedulability. Formal Aspects of Computing, 7(5):510–532, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Liu, Z., Joseph, M. (1997). Formalizing real-time scheduling as program refinement. In: Bertran, M., Rus, T. (eds) Transformation-Based Reactive Systems Development. ARTS 1997. Lecture Notes in Computer Science, vol 1231. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63010-4_20
Download citation
DOI: https://doi.org/10.1007/3-540-63010-4_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63010-4
Online ISBN: 978-3-540-69058-0
eBook Packages: Springer Book Archive