Design Validation using ObjectGEODE

• Verify properties

• Properties describe the needs

• Expressed with

  • Invariants
  • MSCs
  • Observers
    • observers can “inject errors” in the simulation to verify “robustness” of the models
    • computes statistics...

• Design PROOF

  • Errors never occur
  • Needs always fulfilled

SDL Model

Set of MSCs

Invariants

Observers

Proof

Previous slide

Next slide

Back to first slide

View graphic version