Integrating UML with service refinement for requirements modeling and analysis

The Unified Modeling Language (UML) is the de facto standard for requirements modeling and analysis in the software industry. However, it lacks the ability of formal analysis and verification. In this paper, we propose a synthetic approach UML-SR that integrates UML with service refinement (SR) to support the formal requirements modeling and analysis as well as formal verification. The UML-SR requirements model contains a use case diagram, the system sequence diagrams of use cases, a conceptual class diagram, and the formal contracts of system interfaces. To make this integration viable, we extend service refinement with the concepts of visibility in UML. With the visibility extension, we are able to formally specify and verify both internal and external interactions of the system. To demonstrate the effectiveness of our proposed approach, we investigate a case study of an Online Shopping System. The results show that a consistent requirements model can be eventually derived through formal refinement and verification. The proposed approach is useful and can be further applied for the requirements modeling and formal verification in the software industry.