Formal Consistency Verification of UML Requirement and Analysis Models

Formal Consistency Verification of UML Requirement and Analysis Models

Mouez Ali (University of Sfax, Tunisia), Hanene Ben-Abdallah (University of Sfax, Tunisia) and Faïez Gargouri (University of Sfax, Tunisia)
DOI: 10.4018/978-1-4666-4369-7.ch007


To capture and analyze the functional requirements of an information system, UML and the Unified Process (UP) propose the use case and sequence diagrams. However, one of the main difficulties behind the use of UML is how to ensure the consistency of the various diagrams used to model different views of the same system. In this chapter, the authors propose an enriched format for documenting UML2.0 use cases. This format facilitates consistency verification of the functional requirements with respect to the sequence diagrams included in the analysis model. The consistency verification relies on a set of rules to check the correspondence among the elements of the documented use cases and those of the sequence diagrams; the correspondence exploits the implicit semantic relationship between these diagrams as defined in UP. Furthermore, to provide for a rigorous verification, the authors formalize both types of diagrams and their correspondence rules in the formal notation Z. The formal version of the analysis model is then verified through the theorem prover Z/EVES to ensure its consistency.
Chapter Preview

In this section, we first give an overview of requirement modeling in UML according to the UP process. Secondly, we present current proposals for formal analysis of UML models.

Complete Chapter List

Search this Book: