Formalizing and Analyzing UML Use Case Hierarchical Predicate Transition Nets

Abstract

Unified Modeling Language (UML), developed by a group of leading experts in object-oriented methodologies, has become the standard object-oriented development methodology in the software industry. UML contains a set of diagrams for describing different views and aspects of systems. UML use case diagrams are used during requirements analysis to define a use case view that constitutes a system’s functional model. Each use case describes a system’s functionality from a user’s perspective. However, the use case descriptions are often informal, which are error-prone and cannot be formally analyzed to detect problems in user requirements or errors introduced in a system functional model. A well-defined use case view is not only necessary for subsequent correct system design and implementation but also serves as a basis for future system evolution. Therefore, it is extremely important to ensure the correctness of the functional model captured in a use case view. In this chapter, we present an approach to formally translate a use case view into a formal model in hierarchical predicate transition nets that support formal analysis and thus are capable to detect possible requirements and modeling errors in a use case view.