Chapter 8. Typestate Checking