×

Verification of schedulability for real-time programs. (English) Zbl 0838.68078


MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68M20 Performance evaluation, queueing, and scheduling in the context of computer systems
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Audsley, N., Burns, A., Richardson, M., Tindell, K. and Wellings, A.: Applying new scheduling theory to static priority pre-emptive scheduling. Technical Report RTRG/92/120, Department of Computer Science, University of York, 1992.
[2] Abadi, M. and Lamport, L.: The existence of refinement mappings.Theoretical Computer Science, 82(2), May 1991. · Zbl 0728.68083
[3] Abadi, M. and Lamport, L.: An old-fashioned recipe for real-time. In W.R. 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, 1991.
[4] Henzinger, T., Manna, Z. and Pnueli, A.: Temporal proof methodologies for real-time systems. InProceedings of the 8th ACM Annual Symposium on Principles of Programming Languages, pages 269-276, 1991.
[5] Hooman, J.: A denotational real-time semantics for shared processors. InPARLE’91 Parallel Architectures and Languages Europe, Vol. II, Lecture Notes in Computer Science 506, pages 185-201. Springer-Verlag, 1991.
[6] Lamport, L.: A temporal logic of actions. Technical report, Digital SRC, California, April 1990. · Zbl 0699.68044
[7] Liu, Z. and Joseph, M.: Specification and verification of recovery in asynchronous communicating systems. In J. Vytopil, editor,Formal Techniques in Real-Time and Fault Tolerant Systems, pages 137-166. Kluwer Academic Publishers, 1993.
[8] Liu, Z. and Joseph, M.: Stepwise development of fault-tolerant reactive systems. In H. Langmaak, W.-P. de Roever, and J. Vytopil, editors,Formal Techniques in Real-Time and Fault Tolerant Systems, Lecture Notes in Computer Science 863, pages 529-546. Springer-Verlag, 1994.
[9] Zhou, C.C., Hoare, C.A.R. and Ravn, A.P.: A calculus of durations.Information Processing Letters, 40(5), December 1991. · Zbl 0743.68097
[10] Zhou, C.C. Hansen, M.R. Ravn, A.P. and Rischel, H.: Duration specifications for shared processors. In J. Vytopil, editor,Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Computer Science 571. Springer-Verlag, January 1992.
[11] Zhang Y. and Zhou, C.C.: A formal proof of the deadline driven scheduler. In H. Langmaak, W.-P. de Roever, and J. Vytopil, editors,Formal Techniques in Real-Time and Fault Tolerant Systems, Lecture Notes in Computer Science 863, pages 756-775. Springer-Verlag, 1994.
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.