1 Introduction

2 UML State Machines  
2.1 States  
2.2 Behaviors  
2.3 Pseudo States  
2.4 Transitions  
2.5 Deferred Events  
2.6 Run-to-Completion Paradigm

3 Methodology and Categorization Criteria  
3.1 Methodology  
3.2 Categorization

4 The Translation Approaches  
4.1 Translation into Abstract State Machines  
4.2 Translation via Graph Transformation  
4.3 Translation into Automata  
4.4 Translation into Petri Nets  
4.5 Translation into the Input Language of SMV and NuSMV  
4.6 Translation into Process Algebras  
4.7 Translation to PVS, KIV, B and Z  
4.8 Formalization Using Institutions  
4.9 Summary

5 Approaches Providing Operational Semantics for UML State Machines  
5.1 Operational Semantics for UML 1.x  
5.2 Operational Semantics for UML 2.0  
5.3 Operational Semantics for UML 2.1  
5.4 Operational Semantics for UML 2.4  
5.5 Summary

6 Tool Support  
6.1 Surveying Tools for Verifying UML State Machines  
6.2 Summary

7 Related Surveys

8 Conclusion