CSE503: Software Engineering

Analysis of model-based specifications

Why different?

An alternative:
counterexample checking

Why OK?

Nitpick -> Alcoa

An example from Jackson

Basic notions

Object model

Alloy model: declarations

An indicative invariant

A safety condition

Two definitions

Policy invariants

An operation

Analysis strategy

Bug example, implication

Bug example, preservation of invariants

Underlying technology

Unsound, but useful