Getting Level of Specification Right

What's Wrong with This Spec?

Using Swim Lanes

What is a State?

Moore and Mealy

Example: States of the Keypad

Example: States of a Database

ATM with Swim Lanes

Infinite Input States

How ATMs Work (basic)

How ATMs Work (advanced)

Hackers Crack an ATM in Seconds

Automated Attack Synthesis by Extracting Finite State Machines from Protocol Specification Documents