A Gentle Introduction to Modeling, using Alloy

New! Modeling a remote-controlled bathtub and identifying vulnerabilities.

First, special thanks to Daniel Jackson for his incredible patience in answering my endless questions. And, thanks to Daniel and his team for creating such a wonderful and powerful modeling language and tool, Alloy .

Thanks to Charles Wallace for creating this wonderful Alloy Cheat Sheet (Word doc).

Here is a zip file containing all the materials in this Alloy tutorial -- all the Powerpoint slides, examples, and lab exercises.

Table of Contents

  1. [Slides] 10 people coming over for dinner, how will they be seated, can all the seating constraints be satisfied?
  2. [Slides] Alloy is a (fantastic) modeling language and modeling tool ... 3 secrets to understanding Alloy.
  3. [Slides] Farmer needs to ferry a goat, wolf, and cabbage across a river, but his boat can only carry one item at a time.
  4. [Slides] The Einstein puzzle. Einstein said that only 2% of the world could solve it. We will solve it!
  5. [Slides] A step-by-step instruction guide for navigating though Alloy models.
  6. [Slides] I like Alloy because ...
  7. [Slides] Software testing versus Alloy instance generation.
  8. [Slides] Model the cut and paste operations of icons on a desktop.
  9. [Slides] Alloy can tell you whether two models are equivalent - this is really awesome!
  10. [Slides] Creating easy-to-read models.
  11. [Slides] How to implement multiple inheritance in Alloy.
  12. [Slides] What is the universe for your model?
  13. [Slides] Creating high confidence, highly dependable, critical software.
  14. [Slides] Eve steals Alice's password ... how to prevent it.
  15. [Slides] Socrates is mortal ... modeling inferences.
  16. [HTML] The Rule of Maximum Practical Formality.
  17. [Slides] When, What, and Why of creating system and software models.
  18. [Slides] Want to truly understand sets? Learn Alloy! Want to learn Alloy? Learn sets!
  19. [Slides] The root cause of all security failures.
  20. [MS Word] What does it mean to order a set? (Since, by definition, sets are unordered)
  21. [Slides] Object model versus event model
  22. [MS Word] When writing software you must provide a step-by-step set of instructions to the computer. A model of the software, however, doesn’t do that.
  23. [MS Word] Model a green wave - create a model of traffic lights such that drivers encounter a series of green lights.
  24. [Slides] How to implement an encapsulation design in Alloy.
  25. [HTML] SysML versus Alloy.
  26. [HTML] The dirty little lies of the software industry.
  27. [MS Word] Model the binary search algorithm. Dealing with arithmetic overflow.
  28. [Slides] How to ensure each hotel guest has a unique set of keys. Show equivalence of two constraint approaches.
  29. [MS Word] Alloy model of playing tic-tac-toe.
  30. [MS Word] Lessons Learned in Model Building using Alloy.
  31. [Slides] (Part 1) Model Land and Seafloor Surfaces using Alloy.
  32. [Slides] (Part 2) Model Land and Seafloor Surfaces using Alloy.
  33. [Slides] (Part 3) Model Land and Seafloor Surfaces using Alloy.
  34. [MS Word] Alloy versus XML Schema -- infinite loops.
  35. [MS Word] Equivalent logical statements.
  36. [MS Word] Alloy success stories.
  37. [HTML] How to convince management to fund developing Alloy models.
  38. [MS Word] Duality of quantifiers.
  39. [Slides] Registering students for courses, assigning lecturers to courses.
  40. [Slides] Modeling a remote-controlled bathtub and identifying vulnerabilities.

Roger L. Costello
August 28, 2018