Model Checking for UML Use Cases

Summary

A use case driven approach is one of the most practical approaches in object orientation. UML use case diagrams and their descriptions written in a natural language are used in this modeling. Even though this approach provides us with convenient ways to develop large scale software and systems, it seems difficult to assure the correctness of the models, because of insufficient formalization in UML. This paper proposes a formal model verification process for UML use case models. In order to exclude ambiguity from the models, they are firstly formalized using the first order predicate logic. These logic based models are then transformed in the form of Promela code, so that they can be verified using the Spin model checker. A Promela code must be composed based on state transitions, whereas the logic based use case models do not explicitly include the states and their transitions. Therefore we introduce a state identification process in the logic based use case models. A supermarket checkout system is used to show how the proposed process works.