Advertisement

Modeling Concurrency in Dafny

  • K. Rustan M. LeinoEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11174)

Abstract

This article gives a tutorial on how the Dafny language and verifier can be used to model a concurrent system. The running example is a simple ticket system for mutual exclusion. Both safety and, under the assumption of a fair scheduler, liveness are verified.

Notes

Acknowledgments

Andreas Podelski brought up the problem of this ticket system at meeting 54 (Saint Petersburg, Russia, June 2013) of the IFIP Working Group 2.3, where several formalizations were subsequently presented. Xinhaoyuan on github proposed the prefix allowance of conjunctions and disjunctions in Dafny. I thank Shuo Chen for comments on an earlier draft of this article.

References

  1. 1.
    Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRefGoogle Scholar
  2. 2.
    Abrial, J.-R.: Mini-course around Event-B and Rodin, June 2011. https://www.microsoft.com/en-us/research/video/mini-course-around-event-b-and-rodin/
  3. 3.
    Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Softw. Tools Technol. Transf. 12(6), 447–466 (2010)CrossRefGoogle Scholar
  4. 4.
    Back, R.-J., Sere, K.: Action systems with synchronous communication. In: Olderog, E.-R. (ed.) Proceedings of the IFIP TC2/WG2.1/WG2.2/WG2.3 Working Conference on Programming Concepts, Methods and Calculi (PROCOMET 1994). IFIP Transactions, vol. A-56, pp. 107–126. North-Holland, June 1994Google Scholar
  5. 5.
    Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Boston (1988)zbMATHGoogle Scholar
  6. 6.
    Dafny online (2017). http://rise4fun.com/dafny
  7. 7.
    Floyd, R.W.: Assigning meanings to programs. In: Proceedings of the Symposium on Applied Mathematics, vol. 19, pp. 19–32. American Mathematical Society (1967)Google Scholar
  8. 8.
    Gries, D.: The Science of Programming. MCS. Springer-Verlag, New York (1981).  https://doi.org/10.1007/978-1-4612-5983-1CrossRefzbMATHGoogle Scholar
  9. 9.
    Hatcliff, J., Leavens, G.T., Leino, K.R.M., Müller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16:1–16:58 (2012)CrossRefGoogle Scholar
  10. 10.
    Hawblitzel, C., et al.: IronFleet: proving practical distributed systems correct. In: Miller, E.L., Hand, S. (eds.) Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, pp. 1–17. ACM, October 2015Google Scholar
  11. 11.
    Herbert, L., Leino, K.R.M., Quaresma, J.: Using Dafny, an automatic program verifier. In: Meyer, B., Nordio, M. (eds.) LASER 2011. LNCS, vol. 7682, pp. 156–181. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-35746-6_6CrossRefGoogle Scholar
  12. 12.
    Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–583 (1969)CrossRefGoogle Scholar
  13. 13.
    Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)Google Scholar
  14. 14.
    Koenig, J., Leino, K.R.M.: Getting started with Dafny: a guide. In: Nipkow, T., Grumberg, O., Hauptmann, B. (eds.) Software Safety and Security: Tools for Analysis and Verification. NATO Science for Peace and Security Series D: Information and Communication Security, vol. 33, pp. 152–181. IOS Press (2012). Summer School Marktoberdorf 2011 lecture notesGoogle Scholar
  15. 15.
    Lamport, L. (ed.): Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Professional, Boston (2002)Google Scholar
  16. 16.
    Lamport, L.: The TLA+ video course, March 2017. http://lamport.azurewebsites.net/video/videos.html
  17. 17.
    Leino, K.R.M.: Specification and verification of object-oriented software. In: Broy, M., Sitou, W., Hoare, T. (eds.) Engineering Methods and Tools for Software Safety and Security. NATO Science for Peace and Security Series D: Information and Communication Security, vol. 22, pp. 231–266. IOS Press (2009). Summer School Marktoberdorf 2008 lecture notesGoogle Scholar
  18. 18.
    Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-17511-4_20CrossRefzbMATHGoogle Scholar
  19. 19.
    Leino, K.R.M.: Developing verified programs with Dafny. In: Notkin, D., Cheng, B.H.C., Pohl, K. (eds.) 35th International Conference on Software Engineering, ICSE 2013, pp. 1488–1490. IEEE Computer Society (2013)Google Scholar
  20. 20.
    Leino, K.R.M.: Accessible software verification with Dafny. IEEE Software 34(6), 94–97 (2017)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Microsoft ResearchRedmondUSA
  2. 2.Imperial College LondonLondonUK

Personalised recommendations