Skip to main content
SpringerLink
Log in

The Algebra of Multi-tasking

  • Conference paper
  • First Online:
Algebraic Methodology and Software Technology (AMAST 2000)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1816))

Abstract

Modelling multi-tasking behaviour is an important phase of real-time system design. It is shown how task scheduling principles can be captured in a CCS-based process algebra via extensions for both asymmetric interleaving, to model intraprocessor scheduling decisions, and for asynchronous communication, to model interprocessor precedence constraints. Examples are given of task preemption, blocking on shared resources, and multi-task transactions.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. L. Aceto and D. Murphy. Timing and causality in process algebra. Acta Informatica, 33:317–350, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  2. 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.

    Article  Google Scholar 

  3. H. Ben-Abdallah, J.-Y. Choi, D. Clarke, Y. S. Kim, I. Lee, and H.-L. Xie. A process algebraic approach to the schedulability analysis of real-time systems. Real-Time Systems, 15:189–219, 1998.

    Article  Google Scholar 

  4. S. Bornot, J. Sifakis, and S. Tripakis. Modeling urgency in timed systems. In W.-P. de Roever, H. Langmaack, and A. Pnueli, editors, Compositionality: The Significant Difference, volume 1536 of Lecture Notes in Computer Science, pages 103–129. Springer-Verlag, 1998.

    Chapter  Google Scholar 

  5. L. Breveglieri, S. Crespi-Reghizzi, and A. Cherubini. Modeling operating systems schedulers with multi-stack-queue grammars. In G. Ciobanu and G. Păun, editors, Fundamentals of Computation Theory (FCT’99), volume 1684 of Lecture Notes in Computer Science, pages 161–172. Springer-Verlag, 1999.

    Chapter  Google Scholar 

  6. G. C. Buttazzo. Hard Real-Time Computing Systems: Predictable Scheduling Algorithms and Applications. Kluwer, 1997.

    Google Scholar 

  7. J. C. Corbett. Timing analysis of Ada tasking programs. IEEE Transaction on Software Engineering, 22(7):461–483, July 1996.

    Article  Google Scholar 

  8. J. S. Dong, N. Fulton, L. Zucconi, and J. Colton. Formalising process scheduling requirements for an aircraft operational flight program. In Proc. IEEE International Conference on Formal Engineering Methods (ICFEM’97), pages 161–169. IEEE Press, November 1997.

    Google Scholar 

  9. J. D. G. Falardeau. Schedulability analysis in rate monotonic based systems with application to the CF-188. Master’s thesis, Department of Electrical and Computer Engineering, Royal Military College of Canada, May 1994.

    Google Scholar 

  10. C. J. Fidge and J. J. Žic. An expressive real-time CCS. In Proc. Second Australasian Conference on Parallel and Real-Time Systems (PART’95), pages 365–372, Fremantle, September 1995.

    Google Scholar 

  11. P.-A. Hsiung, F. Wang, and Y.-S. Kuo. Scheduling system verification. In W. R. Cleaveland, editor, Tools and Algorithms for the Construction and Analysis of Systems (TACAS’99), volume 1579 of Lecture Notes in Computer Science, pages 19–33. Springer-Verlag, 1999.

    Chapter  Google Scholar 

  12. D. M. Jackson. Experiences in embedded scheduling. In M.-C. Gaudel and J. Woodcock, editors, FME’96: Industrial Benefit and Advances in Formal Methods, volume 1051 of Lecture Notes in Computer Science, pages 445–464. Springer-Verlag, 1996.

    Google Scholar 

  13. J. Jacky. Analyzing a real-time program in Z. In Proc. Z User’s Meeting (ZUM’98), 1998.

    Google Scholar 

  14. Z. Liu, M. Joseph, and T. Janowski. Verification of schedulability for real-time programs. Formal Aspects of Computing, 7(5):510–532, 1995.

    Article  MATH  Google Scholar 

  15. R. Milner. Communication and Concurrency. Prentice-Hall, 1989.

    Google Scholar 

  16. M. Minea. Partial order reduction for model checking of timed automata. In J. C. M. Baeten and S. Mauw, editors, CONCUR’99: Concurrency Theory, volume 1664 of Lecture Notes in Computer Science, pages 431–446. Springer-Verlag, 1999.

    Chapter  Google Scholar 

  17. R. van Glabbeek and P. Rittgen. Scheduling algebra. In A. M. Haeberer, editor, Algebraic Methodology and Software Technology (AMAST’98), volume 1548 of Lecture Notes in Computer Science, pages 278–292. Springer-Verlag, 1999.

    Chapter  Google Scholar 

  18. R. J. van Glabbeek. The meaning of negative premises in transition system specifications II. In F. Meyer auf der Heide and B. Monien, editors, Automata, Languages and Programming, 23rd International Colloquium, volume 1099 of Lecture Notes in Computer Science, pages 502–513. Springer-Verlag, 1996. Extended abstract.

    Google Scholar 

  19. Z. Yuhua and Z. Chaochen. A formal proof of the deadline driven scheduler. In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, Formal Techniques in Real Time and Fault Tolerant Systems, volume 863 of Lecture Notes in Computer Science, pages 756–775. Springer-Verlag, 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Software Verification Research Centre, The University of Queensland, Queensland, 4072, Australia

    Colin J. Fidge

Authors
  1. Colin J. Fidge
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, The University of Iowa, Iowa City, IA, 52242, USA

    Teodor Rus

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fidge, C.J. (2000). The Algebra of Multi-tasking. In: Rus, T. (eds) Algebraic Methodology and Software Technology. AMAST 2000. Lecture Notes in Computer Science, vol 1816. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45499-3_17

Download citation

  • DOI: https://doi.org/10.1007/3-540-45499-3_17

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67530-3

  • Online ISBN: 978-3-540-45499-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation