Our Approach
Executable formal semantics for distributed object systems
- based on rewriting logic
- refined to provide composable service specification units
Basis for
- executable models composed from basic components
- modular formal analysis by
- model checking
- symbolic simulation
- theorem proving