Building Models
• What do we need to know to build a model?
– For model checking we need to specify behavior
• Consider a simple vending machine
– A custome rinserts coins, selects a beverage and receives a can of soda
• Basically a state machine
– Starts in initial state and changes based on user interaction
• We need to know
– What state the vending machine can be in
– How the machine transitions from one state to another
– Where the machine starts