Results
Can analyze a system to detect inconsistencies using commercial model-checking tools
- illegal attachments
- latent deadlocks
- loss of messages
Can check whether all configurations satisfy style constraints
Can prove equivalence between reconfigurable system and static (non-reconfigurable) system