Model Checking

Question 1

Model checking is a tool that provides what?

Answer 1

Provides a way to prove that some properties hold in software

Question 2

What kind of properties would be interesting to prove?

Answer 2

Safety

Liveness

Question 3

What is the overview of model checking?

Answer 3

An automated technique for proving properties of finite state systems

Question 4

Review oven example

Answer 4

Review oven example

Question 5

When making our model, we need to express the ______ ______ and ______

Answer 5

finite states, transitions

Question 6

Models are written often in what?

Answer 6

Formal specification language. Examples include temporal logic, Alloy, TLA, etc

Question 7

Properties in models are often inspired by ________ logic. These constraints express properties interesting to concurrent and distributed systems

Answer 7

temporal

Question 8

What or some examples of temporal constraints for a proposition p?

Answer 8

p will hold eventually in the future
p holds in all future states
p holds in the next state
p holds until another proposition q holds