| Software
model checking |
|
|
|
|
|
|
|
|
|
|
|
|
| • | Finite
state software specifications |
||||||||||
| – | Reactive
systems (avionics, automotive, etc.) |
||||||||||
| – | Hierarchical
state machine specifications |
||||||||||
| • | Not
intended to help with proving |
||||||||||
| consistency
of specification and |
|||||||||||
| implementation |
|||||||||||
| – | Rather,
checking properties of the specification |
||||||||||
| itself |
|||||||||||
