Skip to main content
SpringerLink
Log in

Teaching Concurrency: Theory in Practice

  • Conference paper
Teaching Formal Methods (TFM 2009)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5846))

Included in the following conference series:

Abstract

Teaching courses that rely on sound mathematical principles is nowadays a challenging task at many universities. On the one hand there is an increased demand for educating students in these areas, on the other hand there are more and more students being accepted with less adequate skills in mathematics. We report here on our experiences in teaching concurrency theory over the last twenty years or so to students ranging from mathsphobic bachelor students to sophisticated doctoral students. The contents of the courses, the material on which they are based and the pedagogical philosophy underlying them are described, as well as some of the lessons that we have learned over the years.

The work of Aceto and Ingolfsdottir has been partially supported by the projects “The Equational Logic of Parallel Processes” (nr. 060013021) and “New Developments in Operational Semantics” (nr. 080039021) of the Icelandic Research Fund. Srba was partially supported by Ministry of Education of the Czech Republic, project No. MSM 0021622419.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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.

References

  1. Aceto, L., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, Cambridge (2007)

    MATH  Google Scholar 

  2. Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Comput. Sci. 126(2), 183–235 (1994); Fundamental Study

    Article  MATH  MathSciNet  Google Scholar 

  3. Alur, R., Taubenfeld, G.: Fast timing-based algorithms. Distributed Computing 10(1), 1–10 (1996)

    Article  MathSciNet  Google Scholar 

  4. Andersen, H.R.: An introduction to binary decision diagrams (1998), Version of October 1997 with minor revisions April 1998, p. 36, http://www.itu.dk/people/hra/notes-index.html

  5. Arnold, A., Bégay, D., Crubillé, P.: Construction and Analysis of Transition Systems Using MEC. AMAST Series in Computing, vol. 3. World Scientific, Singapore (1994)

    Google Scholar 

  6. Baeten, J.C., Weijland, P.: Process Algebra. Cambridge Tracts in Theoretical Computer Science, vol. 18. Cambridge University Press, Cambridge (1990)

    Google Scholar 

  7. Bartlett, K., Scantlebury, R., Wilkinson, P.: A note on reliable full–duplex transmission over half–duplex links. Commun. ACM 12, 260–261 (1969)

    Article  Google Scholar 

  8. Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)

    Google Scholar 

  9. Biggs, J.: Teaching for quality learning at University. Open University Press, Stony Stratford (1999)

    Google Scholar 

  10. Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293–318 (1992)

    Article  Google Scholar 

  11. Clarke, E., Emerson, E.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)

    Chapter  Google Scholar 

  12. Clarke, E., Gruemberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  13. Cleaveland, R., Parrow, J., Steffen, B.: The concurrency workbench: A semantics-based tool for the verification of concurrent systems. ACM Trans. Prog. Lang. Syst. 15(1), 36–72 (1993)

    Article  Google Scholar 

  14. Cleaveland, R., Sims, S.: The NCSU Concurrency Workbench. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 394–397. Springer, Heidelberg (1996)

    Google Scholar 

  15. Downey, A.B.: The Little Book of Semaphores, 2nd edn. Green Tea Press (2008), http://www.greenteapress.com/semaphores/

  16. Fokkink, W.: Introduction to Process Algebra. Texts in Theoretical Computer Science. An EATCS Series. Springer, Berlin (2000)

    MATH  Google Scholar 

  17. Hamberg, R., Vaandrager, F.: Using model checkers in an introductory course on operating systems. Operating Systems Review 42(6), 101–111 (2008)

    Article  Google Scholar 

  18. Harel, D., Pnueli, A.: On the development of reactive systems. In: Logics and models of concurrent systems (La Colle-sur-Loup, 1984). NATO Adv. Sci. Inst. Ser. F Comput. Systems Sci., vol. 13, pp. 477–498. Springer, Berlin (1985)

    Google Scholar 

  19. Hennessy, M.: Algebraic Theory of Processes. MIT Press, Cambridge (1988)

    MATH  Google Scholar 

  20. Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137–161 (1985)

    MATH  MathSciNet  Google Scholar 

  21. Hoare, C.: Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs (1985)

    MATH  Google Scholar 

  22. Hurkens, C.: Spreading gossip efficiently. Nieuw Archief voor Wiskunde 5/1(2), 208–210 (2000)

    MathSciNet  Google Scholar 

  23. Ingolfsdottir, A., Godskesen, J.C., Zeeberg, M.: Fra Hennessy-Milner logik til CCS-processer. Master’s thesis, Department of Computer Science, Aalborg University (1987) (in Danish)

    Google Scholar 

  24. Keller, R.: Formal verification of parallel programs. Commun. ACM 19(7), 371–384 (1976)

    Article  MATH  Google Scholar 

  25. Krantz, S.G.: How to Teach Mathematics (a personal pespective). American Mathematical Society, Providence (1993)

    Google Scholar 

  26. Laroussinie, F., Larsen, K.G., Weise, C.: From timed automata to logic - and back. In: Hájek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol. 969, pp. 529–539. Springer, Heidelberg (1995)

    Google Scholar 

  27. Larsen, K.G.: Proof systems for satisfiability in Hennessy–Milner logic with recursion. Theoretical Comput. Sci. 72(2–3), 265–288 (1990)

    Article  MATH  Google Scholar 

  28. Lions, J.L.: ARIANE 5 flight 501 failure: Report by the inquiry board (July 1996), http://www.cs.aau.dk/~luca/SV/ariane.pdf

  29. Magee, J., Kramer, J.: Concurrency: State Models and Java Programs. John Wiley, Chichester (1999)

    MATH  Google Scholar 

  30. Mazur, E.: Peer Instruction: A User’s Manual. Series in Educational Innovation. Prentice-Hall International, Upper Saddle River (1997)

    Google Scholar 

  31. Milner, R.: Communication and Concurrency. Prentice-Hall International, Englewood Cliffs (1989)

    MATH  Google Scholar 

  32. Papadimitriou, C.H.: Mythematics: storytelling in the teaching of computer science and mathematics. In: Dagdilelis, V., Satratzemi, M., Finkel, D., Boyle, R.D., Evangelidis, G. (eds.) Proceedings of the 8th Annual SIGCSE Conference on Innovation and Technology in Computer Science Education, ITiCSE 2003, Thessaloniki, Greece, June 30–July 2, p. 1. ACM, New York (2003)

    Google Scholar 

  33. Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)

    Chapter  Google Scholar 

  34. Patterson, D.A.: 20\(^{\mbox{th}}\) century vs. 21\(^{\mbox{st}}\) century C&C: The SPUR manifesto. Commun. ACM 48(3), 15–16 (2005)

    Article  Google Scholar 

  35. Pnueli, A.: The temporal logic of programs. In: Proceedings \(\it 18^{th}\) Annual Symposium on Foundations of Computer Science, pp. 46–57. IEEE, Los Alamitos (1977)

    Google Scholar 

  36. Pratt, V.R.: Anatomy of the Pentium bug. In: Mosses, P.D., Schwartzbach, M.I., Nielsen, M. (eds.) CAAP 1995, FASE 1995, and TAPSOFT 1995. LNCS, vol. 915, pp. 97–107. Springer, Heidelberg (1995)

    Google Scholar 

  37. Roscoe, B.: The Theory and Practice of Concurrency. Prentice-Hall International, Englewood Cliffs (1999)

    Google Scholar 

  38. Schneider, S.: Concurrent and Real-time Systems: The CSP Approach. John Wiley, Chichester (1999)

    Google Scholar 

  39. Steffen, B., Ingolfsdottir, A.: Characteristic formulae for processes with divergence. Information and Computation 110(1), 149–163 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  40. Stirling, C.: Local model checking games. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 1–11. Springer, Heidelberg (1995)

    Google Scholar 

  41. Stirling, C.: Modal and Temporal Properties of Processes. Springer, Heidelberg (2001)

    Google Scholar 

  42. Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics 5, 285–309 (1955)

    MATH  MathSciNet  Google Scholar 

  43. Thomas, W.: On the Ehrenfeucht-Fraïssé game in theoretical computer science (extended abstract). In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993, FASE 1993, and TAPSOFT 1993. LNCS, vol. 668, pp. 559–568. Springer, Heidelberg (1993)

    Google Scholar 

  44. Walker, D.: Automated analysis of mutual exclusion algorithms using CCS. Journal of Formal Aspects of Computing Science 1, 273–292 (1989)

    Article  Google Scholar 

  45. Yi, W.: Real-time behaviour of asynchronous agents. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 502–520. Springer, Heidelberg (1990)

    Google Scholar 

  46. Yi, W.: A Calculus of Real Time Systems. PhD thesis, Chalmers University of Technology, Göteborg, Sweden (1991)

    Google Scholar 

  47. Yi, W.: CCS + time = an interleaving model for real time systems. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol. 510, pp. 217–228. Springer, Heidelberg (1991)

    Google Scholar 

  48. Yoshigahara, N.: Rush Hour, Traffic Jam Puzzle, http://www.puzzles.com/products/rushhour.htm by Puzzles.com (accessed on July 10th, 2009)

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, Reykjavik University, Kringlan 1, 103, Reykjavik, Iceland

    Luca Aceto & Anna Ingolfsdottir

  2. Department of Computer Science, Aalborg University, Selma Lagerlöfs Vej 300, 9220, Aalborg Ø, Denmark

    Kim G. Larsen & Jiří Srba

Authors
  1. Luca Aceto
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Anna Ingolfsdottir
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Kim G. Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jiří Srba
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computing Laboratory, Oxford University, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK

    Jeremy Gibbons

  2. Departamento de Informática, Universidade do Minho, Campus de Gualtar, 4710-057, Braga, Portugal

    José Nuno Oliveira

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Aceto, L., Ingolfsdottir, A., Larsen, K.G., Srba, J. (2009). Teaching Concurrency: Theory in Practice. In: Gibbons, J., Oliveira, J.N. (eds) Teaching Formal Methods. TFM 2009. Lecture Notes in Computer Science, vol 5846. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04912-5_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-04912-5_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-04911-8

  • Online ISBN: 978-3-642-04912-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation