Software model checking
Finite state software specifications
- Reactive systems (avionics, automotive, etc.)
- Hierarchical state machine specifications
- Statecharts (Harel), RSML (Leveson)
Goal: increase confidence in the correctness of the specification