Benefits
Executable specification
- formally based
- bridging the gap between code and model-checking abstractions
Starting point for a wide spectrum of analyses
- default execution
- scenario based execution
- model-checking and symbolic simulation
- theorem prov ing
Framework for studying composition / interoperation of different protocols