Abstract
We show how real-time schedulability tests and program refinement rules can be integrated to create a formal development method of practical use to real-time programmers. A computational model for representing task scheduling is developed within a ⋆imed’ refinement calculus. Proven multi-tasking schedulability tests then become available as feasibility checks during system refinement.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
N. Audsley, A. Burns, M. Richardson, K. Tindell, and A. Wellings. Applying new scheduling theory to static priority pre-emptive scheduling. Software Engineering Journal, 8(5):284–292, September 1993.
T.P. Baker. Stack-based scheduling of real-time processes. Real Time Systems, 3(1):67–99, March 1991.
J. Bowen, editor. Towards Verified Systems, volume 2 of Real-Time Safety Critical Systems. Elsevier, 1994.
A. Burns and A. Wellings. Real-Time Systems and their Programming Languages. Addison-Wesley, 1990.
A. Burns and A.J. Wellings. Priority inheritance and message passing communication: A formal treatment. The Journal of Real-Time Systems, 3:19–44, 1991.
C. Fidge. Adding real time to formal program development. In M. Naftalin, T. Denvir, and M. Bertran, editors, FME'94: Industrial Benefit of Formal Methods, volume 873 of Lecture Notes in Computer Science, pages 618–638. Springer-Verlag, 1994.
J. Hooman. Extending Hoare logic to real-time. Formal Aspects of Computing, 6(6A):801–825, 1994.
Ada 9X Mapping/Revision Team Intermetrics. Ada 9X reference manual, draft version 5.0, June 1994.
H. Jifeng. Provably Correct Systems. McGraw-Hill, 1995.
B. Mahony. Using the refinement calculus for dataflow processes. Technical Report TR 94-32, Software Verification Research Centre, October 1994.
B. Mahony. Networks of predicate transformers. Technical Report TR 95-5, Software Verification Research Centre, February 1995.
M. Pilling, A. Burns, and K. Raymond. Formal specifications and proofs of inheritance protocols for real-time scheduling. Software Engineering Journal, 5(5), September 1990.
D. Scholefield. Proving properties of real-time semaphores. Science of Computer Programming, 24(2):159–181, April 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fidge, C., Utting, M., Kearney, P., Hayes, I. (1996). Integrating real-time scheduling theory and program refinement. In: Gaudel, MC., Woodcock, J. (eds) FME'96: Industrial Benefit and Advances in Formal Methods. FME 1996. Lecture Notes in Computer Science, vol 1051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60973-3_95
Download citation
DOI: https://doi.org/10.1007/3-540-60973-3_95
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60973-5
Online ISBN: 978-3-540-49749-3
eBook Packages: Springer Book Archive