Analysis strategy
•
Check consistency
–
Ask for instances of states and transitions
•
Check consequences
–
Assert implications of invariants
–
Assert properties of invariants (for instance,
preservation of invariants)