A Multiview Formal Model of Use Case Diagrams Using Z Notation: Towards Improving Functional Requirements Quality

We propose a new formal model of UML use case diagram using Z notation to address some of its shortcomings. UML use case diagram has therefore become commonly used to structure functional requirements and the greatest challenge facing the software developer nowadays is to deliver a high quality product meeting customers’ requirements. However, the major disadvantage of UML models is their imprecision. In addition, they are basically in a form of semiformal modelling representations and associated natural language requirements and lack any mechanism to rigorously check consistency which results in its models being subject to ambiguity. This paper reports on the first formal modelling approach of use case diagrams in a multiview context. The approach is divided into two steps. In the first step, a formal model of UML use case diagram is proposed using Z notation. Then, a multiview consistency checking is presented. This approach guarantees software consistency, improving requirements quality.