 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| • |
The
goal of model checking is to allow finite state
|
|
|
descriptions
to be analyzed and shown to have particular
|
|
|
desirable
properties
|
|
|
|
– |
Won’t
help when you don’t want or need finite state descriptions
|
|
|
|
– |
Definitely
added value when you do, but it’s not turnkey yet
|
|
|
|
• |
There’s
still a real art in managing model checking
|
|
|
|
– |
Definitely
feasible on modest sized systems
|
|
|
| • |
This
was fast: my goal wasn’t to make you into model
|
|
|
checking
experts
|
|
|
|
– |
But
it might titillate one or two of you to learn more
|
|
|
| • |
But
rather to understand the sketches of what model
|
|
|
checking
is and why it is so promising for checking some
|
|
classes
of specifications
|
|