- Identify variables that form state
- Identify invariants
- Policy for concurrent access to state (synchronization policy)
- Synchronization Policy preserves invariants and post-conditions
Final
allows to reduce state space- Illegal states need to be prevented by synchronizing involved variables