SPIN:
• SPIN generates C program that is the model checker 
– The pan verifier
• Process Analyzer 
– Run the pan executable to do the model checking
• SPIN simulation modes 
– Random: SPIN randomly makes decisions 
– Interactive: User interactively makes decisions 
– Guided: Analyze failed verification
• Trail files