WHY USE FORMAL ASSERTIONS?
- Discover errors and flaws at the model and specification level
- Compensate for ambiguities of natural language used in the informal definitions of concepts
- Detect model incompleteness by identifying missing concepts or associations
- Enable use of tools capable of analysing formal specifications (model checkers, animators, …)
FORMAL ASSERTIONS IN OBJECTIVER
- Embedded in the model as specific attributes
- Formal definition for Goals and Objects
- Pre- and postconditions for Operations
- Domain (off-the shelf behaviors)
- Required (behavior strengthening to satisfy requirements)
- No predefined formal language in standard
- Plugin approach to support specific languages
USE PLUGIN FOR OCL SUPPORT
- For Desktop editions only
- OCL expressions embedded in the model
- OCL Invariants on objects
- OCL Pre- and postconditions on operations performed by agents
- Non-liveness requirements and domain properties as OCL invariants
- Traceability between goal model assertions and operational model assertions
- USE generator producing specifications that can be loaded in the USE environment
- OCL Syntax checking
- Selective export excluding discarded branches of alternatives
