CSE503: Software Engineering

Question

Standard answers include

An alternative: model checking

State Transition Graph

Example

A computation tree

Temporal formulae:
we can say things like

Mutual exclusion example

How does model checking work? (in brief!)

Example

Example

Symbolic model checking

Binary decision diagrams (BDDs)

BDD-based model checking

BDD-based successes in HW

Software model checking

Why might it fail?

Our approach at UW—try it!

TCAS

TCAS specification

TCAS—high-level structure

Using SMV

Iterative process

Use of non-determinism:
needed to reduce size of the BDDs

Checking properties

Property checking

Disclaimer

Deterministic transitions

Slide 30

Function consistency

Slide 32

Display_Model_Goal

Output agreement

Output agreement check

Limitations

Whence formulae?

Whence formulae?

What about infinite state?

Model checking wrap up