\documentclass[11pt,twoside]{article}\makeatletter

\IfFileExists{xcolor.sty}%
  {\RequirePackage{xcolor}}%
  {\RequirePackage{color}}
\usepackage{colortbl}
\usepackage{wrapfig}
\usepackage{ifxetex}
\ifxetex
  \usepackage{fontspec}
  \usepackage{xunicode}
  \catcode`⃥=\active \def⃥{\textbackslash}
  \catcode`❴=\active \def❴{\{}
  \catcode`❵=\active \def❵{\}}
  \def\textJapanese{\fontspec{Noto Sans CJK JP}}
  \def\textChinese{\fontspec{Noto Sans CJK SC}}
  \def\textKorean{\fontspec{Noto Sans CJK KR}}
  \setmonofont{DejaVu Sans Mono}
  
\else
  \IfFileExists{utf8x.def}%
   {\usepackage[utf8x]{inputenc}
      \PrerenderUnicode{–}
    }%
   {\usepackage[utf8]{inputenc}}
  \usepackage[english]{babel}
  \usepackage[T1]{fontenc}
  \usepackage{float}
  \usepackage[]{ucs}
  \uc@dclc{8421}{default}{\textbackslash }
  \uc@dclc{10100}{default}{\{}
  \uc@dclc{10101}{default}{\}}
  \uc@dclc{8491}{default}{\AA{}}
  \uc@dclc{8239}{default}{\,}
  \uc@dclc{20154}{default}{ }
  \uc@dclc{10148}{default}{>}
  \def\textschwa{\rotatebox{-90}{e}}
  \def\textJapanese{}
  \def\textChinese{}
  \IfFileExists{tipa.sty}{\usepackage{tipa}}{}
\fi
\def\exampleFont{\ttfamily\small}
\DeclareTextSymbol{\textpi}{OML}{25}
\usepackage{relsize}
\RequirePackage{array}
\def\@testpach{\@chclass
 \ifnum \@lastchclass=6 \@ne \@chnum \@ne \else
  \ifnum \@lastchclass=7 5 \else
   \ifnum \@lastchclass=8 \tw@ \else
    \ifnum \@lastchclass=9 \thr@@
   \else \z@
   \ifnum \@lastchclass = 10 \else
   \edef\@nextchar{\expandafter\string\@nextchar}%
   \@chnum
   \if \@nextchar c\z@ \else
    \if \@nextchar l\@ne \else
     \if \@nextchar r\tw@ \else
   \z@ \@chclass
   \if\@nextchar |\@ne \else
    \if \@nextchar !6 \else
     \if \@nextchar @7 \else
      \if \@nextchar (8 \else
       \if \@nextchar )9 \else
  10
  \@chnum
  \if \@nextchar m\thr@@\else
   \if \@nextchar p4 \else
    \if \@nextchar b5 \else
   \z@ \@chclass \z@ \@preamerr \z@ \fi \fi \fi \fi
   \fi \fi  \fi  \fi  \fi  \fi  \fi \fi \fi \fi \fi \fi}
\gdef\arraybackslash{\let\\=\@arraycr}
\def\@textsubscript#1{{\m@th\ensuremath{_{\mbox{\fontsize\sf@size\z@#1}}}}}
\def\Panel#1#2#3#4{\multicolumn{#3}{){\columncolor{#2}}#4}{#1}}
\def\abbr{}
\def\corr{}
\def\expan{}
\def\gap{}
\def\orig{}
\def\reg{}
\def\ref{}
\def\sic{}
\def\persName{}\def\name{}
\def\placeName{}
\def\orgName{}
\def\textcal#1{{\fontspec{Lucida Calligraphy}#1}}
\def\textgothic#1{{\fontspec{Lucida Blackletter}#1}}
\def\textlarge#1{{\large #1}}
\def\textoverbar#1{\ensuremath{\overline{#1}}}
\def\textquoted#1{‘#1’}
\def\textsmall#1{{\small #1}}
\def\textsubscript#1{\@textsubscript{\selectfont#1}}
\def\textxi{\ensuremath{\xi}}
\def\titlem{\itshape}
\newenvironment{biblfree}{}{\ifvmode\par\fi }
\newenvironment{bibl}{}{}
\newenvironment{byline}{\vskip6pt\itshape\fontsize{16pt}{18pt}\selectfont}{\par }
\newenvironment{citbibl}{}{\ifvmode\par\fi }
\newenvironment{docAuthor}{\ifvmode\vskip4pt\fontsize{16pt}{18pt}\selectfont\fi\itshape}{\ifvmode\par\fi }
\newenvironment{docDate}{}{\ifvmode\par\fi }
\newenvironment{docImprint}{\vskip 6pt}{\ifvmode\par\fi }
\newenvironment{docTitle}{\vskip6pt\bfseries\fontsize{22pt}{25pt}\selectfont}{\par }
\newenvironment{msHead}{\vskip 6pt}{\par}
\newenvironment{msItem}{\vskip 6pt}{\par}
\newenvironment{rubric}{}{}
\newenvironment{titlePart}{}{\par }

\newcolumntype{L}[1]{){\raggedright\arraybackslash}p{#1}}
\newcolumntype{C}[1]{){\centering\arraybackslash}p{#1}}
\newcolumntype{R}[1]{){\raggedleft\arraybackslash}p{#1}}
\newcolumntype{P}[1]{){\arraybackslash}p{#1}}
\newcolumntype{B}[1]{){\arraybackslash}b{#1}}
\newcolumntype{M}[1]{){\arraybackslash}m{#1}}
\definecolor{label}{gray}{0.75}
\def\unusedattribute#1{\sout{\textcolor{label}{#1}}}
\DeclareRobustCommand*{\xref}{\hyper@normalise\xref@}
\def\xref@#1#2{\hyper@linkurl{#2}{#1}}
\begingroup
\catcode`\_=\active
\gdef_#1{\ensuremath{\sb{\mathrm{#1}}}}
\endgroup
\mathcode`\_=\string"8000
\catcode`\_=12\relax

\usepackage[a4paper,twoside,lmargin=1in,rmargin=1in,tmargin=1in,bmargin=1in,marginparwidth=0.75in]{geometry}
\usepackage{framed}

\definecolor{shadecolor}{gray}{0.95}
\usepackage{longtable}
\usepackage[normalem]{ulem}
\usepackage{fancyvrb}
\usepackage{fancyhdr}
\usepackage{graphicx}
\usepackage{marginnote}

\renewcommand{\@cite}[1]{#1}


\renewcommand*{\marginfont}{\itshape\footnotesize}

\def\Gin@extensions{.pdf,.png,.jpg,.mps,.tif}

  \pagestyle{fancy}

\usepackage[pdftitle={Towards Verification of UML Class Models using Formal Specification Methods: A Review},
 pdfauthor={}]{hyperref}
\hyperbaseurl{}

	 \paperwidth210mm
	 \paperheight297mm
              
\def\@pnumwidth{1.55em}
\def\@tocrmarg {2.55em}
\def\@dotsep{4.5}
\setcounter{tocdepth}{3}
\clubpenalty=8000
\emergencystretch 3em
\hbadness=4000
\hyphenpenalty=400
\pretolerance=750
\tolerance=2000
\vbadness=4000
\widowpenalty=10000

\renewcommand\section{\@startsection {section}{1}{\z@}%
     {-1.75ex \@plus -0.5ex \@minus -.2ex}%
     {0.5ex \@plus .2ex}%
     {\reset@font\Large\bfseries}}
\renewcommand\subsection{\@startsection{subsection}{2}{\z@}%
     {-1.75ex\@plus -0.5ex \@minus- .2ex}%
     {0.5ex \@plus .2ex}%
     {\reset@font\Large}}
\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}%
     {-1.5ex\@plus -0.35ex \@minus -.2ex}%
     {0.5ex \@plus .2ex}%
     {\reset@font\large}}
\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}%
     {-1ex \@plus-0.35ex \@minus -0.2ex}%
     {0.5ex \@plus .2ex}%
     {\reset@font\normalsize}}
\renewcommand\subparagraph{\@startsection{subparagraph}{5}{\parindent}%
     {1.5ex \@plus1ex \@minus .2ex}%
     {-1em}%
     {\reset@font\normalsize\bfseries}}


\def\l@section#1#2{\addpenalty{\@secpenalty} \addvspace{1.0em plus 1pt}
 \@tempdima 1.5em \begingroup
 \parindent \z@ \rightskip \@pnumwidth 
 \parfillskip -\@pnumwidth 
 \bfseries \leavevmode #1\hfil \hbox to\@pnumwidth{\hss #2}\par
 \endgroup}
\def\l@subsection{\@dottedtocline{2}{1.5em}{2.3em}}
\def\l@subsubsection{\@dottedtocline{3}{3.8em}{3.2em}}
\def\l@paragraph{\@dottedtocline{4}{7.0em}{4.1em}}
\def\l@subparagraph{\@dottedtocline{5}{10em}{5em}}
\@ifundefined{c@section}{\newcounter{section}}{}
\@ifundefined{c@chapter}{\newcounter{chapter}}{}
\newif\if@mainmatter 
\@mainmattertrue
\def\chaptername{Chapter}
\def\frontmatter{%
  \pagenumbering{roman}
  \def\thechapter{\@roman\c@chapter}
  \def\theHchapter{\roman{chapter}}
  \def\thesection{\@roman\c@section}
  \def\theHsection{\roman{section}}
  \def\@chapapp{}%
}
\def\mainmatter{%
  \cleardoublepage
  \def\thechapter{\@arabic\c@chapter}
  \setcounter{chapter}{0}
  \setcounter{section}{0}
  \pagenumbering{arabic}
  \setcounter{secnumdepth}{6}
  \def\@chapapp{\chaptername}%
  \def\theHchapter{\arabic{chapter}}
  \def\thesection{\@arabic\c@section}
  \def\theHsection{\arabic{section}}
}
\def\backmatter{%
  \cleardoublepage
  \setcounter{chapter}{0}
  \setcounter{section}{0}
  \setcounter{secnumdepth}{2}
  \def\@chapapp{\appendixname}%
  \def\thechapter{\@Alph\c@chapter}
  \def\theHchapter{\Alph{chapter}}
  \appendix
}
\newenvironment{bibitemlist}[1]{%
   \list{\@biblabel{\@arabic\c@enumiv}}%
       {\settowidth\labelwidth{\@biblabel{#1}}%
        \leftmargin\labelwidth
        \advance\leftmargin\labelsep
        \@openbib@code
        \usecounter{enumiv}%
        \let\p@enumiv\@empty
        \renewcommand\theenumiv{\@arabic\c@enumiv}%
	}%
  \sloppy
  \clubpenalty4000
  \@clubpenalty \clubpenalty
  \widowpenalty4000%
  \sfcode`\.\@m}%
  {\def\@noitemerr
    {\@latex@warning{Empty `bibitemlist' environment}}%
    \endlist}

\def\tableofcontents{\section*{\contentsname}\@starttoc{toc}}
\parskip0pt
\parindent1em
\def\Panel#1#2#3#4{\multicolumn{#3}{){\columncolor{#2}}#4}{#1}}
\newenvironment{reflist}{%
  \begin{raggedright}\begin{list}{}
  {%
   \setlength{\topsep}{0pt}%
   \setlength{\rightmargin}{0.25in}%
   \setlength{\itemsep}{0pt}%
   \setlength{\itemindent}{0pt}%
   \setlength{\parskip}{0pt}%
   \setlength{\parsep}{2pt}%
   \def\makelabel##1{\itshape ##1}}%
  }
  {\end{list}\end{raggedright}}
\newenvironment{sansreflist}{%
  \begin{raggedright}\begin{list}{}
  {%
   \setlength{\topsep}{0pt}%
   \setlength{\rightmargin}{0.25in}%
   \setlength{\itemindent}{0pt}%
   \setlength{\parskip}{0pt}%
   \setlength{\itemsep}{0pt}%
   \setlength{\parsep}{2pt}%
   \def\makelabel##1{\upshape ##1}}%
  }
  {\end{list}\end{raggedright}}
\newenvironment{specHead}[2]%
 {\vspace{20pt}\hrule\vspace{10pt}%
  \phantomsection\label{#1}\markright{#2}%

  \pdfbookmark[2]{#2}{#1}%
  \hspace{-0.75in}{\bfseries\fontsize{16pt}{18pt}\selectfont#2}%
  }{}
      \def\TheFullDate{1970-01-01 (revised: 01 January 1970)}
\def\TheID{\makeatother }
\def\TheDate{1970-01-01}
\title{Towards Verification of UML Class Models using Formal Specification Methods: A Review}
\author{}\makeatletter 
\makeatletter
\newcommand*{\cleartoleftpage}{%
  \clearpage
    \if@twoside
    \ifodd\c@page
      \hbox{}\newpage
      \if@twocolumn
        \hbox{}\newpage
      \fi
    \fi
  \fi
}
\makeatother
\makeatletter
\thispagestyle{empty}
\markright{\@title}\markboth{\@title}{\@author}
\renewcommand\small{\@setfontsize\small{9pt}{11pt}\abovedisplayskip 8.5\p@ plus3\p@ minus4\p@
\belowdisplayskip \abovedisplayskip
\abovedisplayshortskip \z@ plus2\p@
\belowdisplayshortskip 4\p@ plus2\p@ minus2\p@
\def\@listi{\leftmargin\leftmargini
               \topsep 2\p@ plus1\p@ minus1\p@
               \parsep 2\p@ plus\p@ minus\p@
               \itemsep 1pt}
}
\makeatother
\fvset{frame=single,numberblanklines=false,xleftmargin=5mm,xrightmargin=5mm}
\fancyhf{} 
\setlength{\headheight}{14pt}
\fancyhead[LE]{\bfseries\leftmark} 
\fancyhead[RO]{\bfseries\rightmark} 
\fancyfoot[RO]{}
\fancyfoot[CO]{\thepage}
\fancyfoot[LO]{\TheID}
\fancyfoot[LE]{}
\fancyfoot[CE]{\thepage}
\fancyfoot[RE]{\TheID}
\hypersetup{citebordercolor=0.75 0.75 0.75,linkbordercolor=0.75 0.75 0.75,urlbordercolor=0.75 0.75 0.75,bookmarksnumbered=true}
\fancypagestyle{plain}{\fancyhead{}\renewcommand{\headrulewidth}{0pt}}

\date{}
\usepackage{authblk}

\providecommand{\keywords}[1]
{
\footnotesize
  \textbf{\textit{Index terms---}} #1
}

\usepackage{graphicx,xcolor}
\definecolor{GJBlue}{HTML}{273B81}
\definecolor{GJLightBlue}{HTML}{0A9DD9}
\definecolor{GJMediumGrey}{HTML}{6D6E70}
\definecolor{GJLightGrey}{HTML}{929497} 

\renewenvironment{abstract}{%
   \setlength{\parindent}{0pt}\raggedright
   \textcolor{GJMediumGrey}{\rule{\textwidth}{2pt}}
   \vskip16pt
   \textcolor{GJBlue}{\large\bfseries\abstractname\space}
}{%   
   \vskip8pt
   \textcolor{GJMediumGrey}{\rule{\textwidth}{2pt}}
   \vskip16pt
}

\usepackage[absolute,overlay]{textpos}

\makeatother 
      \usepackage{lineno}
      \linenumbers
      
\begin{document}

             \author[1]{Kruti P.  Shah}

             \author[2]{Emanuel S.  Grant}

\renewcommand\Authands{ and }

\date{\small \em Received: 1 January 1970 Accepted: 1 January 1970 Published: 1 January 1970}

\maketitle


\begin{abstract}
        


Abstractâ??" In today's world, many elements of our lives are being affected by software and for that we are in greater need of high-quality software. The Unified Modeling Language (UML) is considered the de facto standard for object-oriented software model development. UML class diagram plays an important role in the design and specification of software systems. A class diagram provides a static description of system components.

\end{abstract}


\keywords{formal methods; model verification; MDE; UML models; UML class diagrams}

\begin{textblock*}{18cm}(1cm,1cm) % {block width} (coords) 
\textcolor{GJBlue}{\LARGE Global Journals \LaTeX\ JournalKaleidoscope\texttrademark}
\end{textblock*}

\begin{textblock*}{18cm}(1.4cm,1.5cm) % {block width} (coords) 
\textcolor{GJBlue}{\footnotesize \\ Artificial Intelligence formulated this projection for compatibility purposes from the original article published at Global Journals. However, this technology is currently in beta. \emph{Therefore, kindly ignore odd layouts, missed formulae, text, tables, or figures.}}
\end{textblock*}


\begin{textblock*}{10cm}(1.05cm,3cm)
{{\textit{CrossRef DOI of original article:}} \underline{}}
\end{textblock*}\let\tabcellsep& 	 	 		 
\section[{Introduction}]{Introduction}\par
raphical models of software systems are designed and developed in the initial phase of the Software Development Life Cycle (SDLC) \hyperref[b0]{[1]}. A model is an abstract representation that is used to analyse and understand a different aspect of software system \hyperref[b1]{[2]}. In Model-Driven Engineering (MDE), the software design model is considered a foundation of all development activities. Models in software engineering are used to elicit requirements, design the system, and develop the code of the proposed system.\par
In software engineering, it is essential and beneficial to design a model before the implementation.\par
It provides an understandable view of the system and improves communication among technical developers and non-technical users. Along with that, the software design model provides identification of ambiguities and uncertainties at the initial level of SDLC with the help of model verification techniques \hyperref[b2]{[3,}\hyperref[b3]{4]}.\par
Unified Modeling Language (UML) \hyperref[b1]{[2]} is a widely used graphical modeling language, and it is extensively used in MDE. It is used to specify, simulate, and construct software system components. The UML has been adopted and standardized by the Object Modeling Group \hyperref[b4]{[5]}. It has many static and dynamic models for dealing with different aspects of software.\par
The class model is an essential part of UML which performs a major role in analysis and design of software \hyperref[b4]{[5]}.This work considers the UML class diagram, which is the most fundamental and widely used among all UML models according to a survey presented in \hyperref[b5]{[6]}. A Class Diagram provides a static description of system components. The key components of a class model are classes with their attributes and methods, hierarchy (generalization) class relationships, and associations (general, aggregation, and composition) \hyperref[b1]{[2,}\hyperref[b6]{7]}.\par
UML is considered the standard for objectoriented software model development that allows modeling of various aspects of complex systems \hyperref[b1]{[2,}\hyperref[b6]{7]}. However, there are many concepts in the UML with imprecise semantics, which limit the use of the UML and reduce the quality of the UML models. Also, they lack a formal foundation. Therefore, model verification is not possible in them. Thus, developing technologies for the analysis and verification of UML models is significant to developers who use UML for system modeling.\par
The programming language code is developed with the reference of the design models in MDE, and defects and ambiguities in the model can implicitly transfer into the programming code, making it more difficult to determine and rectify. Also, the development of these models is a highly time-intensive process. Therefore, it is extremely important to check the correctness of these models and identify the problems in the early stage of the software design process.\par
Model verification ensures that the design model is unambiguous, correct, and bug-free. It essentially verifies the model's accuracy and guarantees that the model is consistent and acceptable. The ability to analyse and validate UML models is provided by formal specification methods \hyperref[b7]{[8]}. Formal methods involve the use of a specification language and mathematical theories to design models. They enhance consistency, eliminate design flaws, and improve system reliability.\par
Despite the challenges that model complexity has introduced into MDE-based software development processes, as well as the benefits of using formal methods to verify software, there has been a lot of work done on applying formal methods and formal analysis techniques to ensure the model correctness.\par
This paper reviews the progress of some research articles on UML class model verification methods Z(zed) and Object Constraint Language (OCL) and directs future research in the area of formal specification language. The primary goal of this work is to provide a summary of approaches considered in selected articles, along with the quality of their results and conclusions. This review will be useful for researchers to understand the important open issues in existing methods and limitations that need to be addressed in the area of model correctness.\par
The remainder of the paper is organized as follows. Section 2 represents the review process including the research questions and the inclusion/exclusion criteria. Section 3 gives a brief theoretical background of UML class model along with the model transformation and formal methods to verify the correctness of UML models. Section 4discusses the studies and work done in the area of verification and correctness of UML class models using formal methods. Section 5 discusses the review summary and important open issues in the domain of formal specification methods followed by the conclusion. 
\section[{II.}]{II.} 
\section[{Review Process}]{Review Process}\par
This section discusses the Research Questions followed by defining inclusion and exclusion criteria for the review. 
\section[{a) Research Questions}]{a) Research Questions}\par
This paper focuses on providing an analysis and comparison of the research initiatives done in the field of formal verification approaches mainly Z(zed) notation and Object Constraint Language (OCL). More precisely, we aim to answer the following research questions in this literature review: RQ1: 
\section[{Theoretical Background}]{Theoretical Background}\par
This section covers some of the theories and prior work in the area of UML models and various aspects of UML class diagrams along with the description of the requirement of model transformation and formal specification methods to verify the correctness of such models.  
\section[{H b) Inclusion/Exclusion Criteria}]{H b) Inclusion/Exclusion Criteria}\par
In this section, we defined inclusion/exclusion criteria to determine the related works. The inclusion criteria focus on: 1)studies related to the verification of UML class model using formal methods Z and OCL and 2) paper published in English. On the other hand, We exclude the formal verification studies that are related to dynamic UML models. Based on the inclusion/exclusion criteria, I have selected following studies that are related to the Z-notation and OCL for this review. 
\section[{a) Unified Modeling Language (UML)}]{a) Unified Modeling Language (UML)}\par
UML \hyperref[b1]{[2,}\hyperref[b6]{7]} has been widely accepted as the standard language for modeling and documenting software systems. Their significance has been enhanced with the beginning of the Model-Driven Development (MDD) approach, in which analysis and design models play an essential role in the process of software development. The UML offers a number of diagram forms to describe particular aspects of software artifacts. These diagram structures can be divided into two categories static or dynamic views:\par
Static view: It describes the structural aspect of the system and its components. It includes objects, classes, attributes, operations, and their inter-relationships. The structural view can be represented by class diagrams and composite structure diagrams.\par
Dynamic view: It describes the behavioral aspect of the system. The dynamic view reflects the changes related to the internal states of individual objects and changes in the system's overall state. This view can be represented by sequence, activity, and state chart diagrams. 
\section[{i. UML Class Diagram}]{i. UML Class Diagram}\par
The UML class diagrams are used to represent the static structure of system components \hyperref[b1]{[2,}\hyperref[b6]{7]}. It describes the system structure in terms of classes, attributes, and constraints imposed on classes (operations) and their inter-relationships.This work focuses on the use of the UML class diagrams. Class diagrams are used at the analysis phase to present a view of the static entities in the problem domain, and at the design phase to present a view of the static entities (classifiers) in the solution domain. A class diagram is best described as a set of graph elements connected by their relationships.\par
Classes in UML models are represented as rectangles. Each class consists of a name, set of attributes, and set of operations on the class's attributes. Figure  {\ref 1} shows an example of a class diagram consisting of classes, associations (aggregations and compositions), and generalizations.\par
ii 
\section[{. UML Association (Aggregation, Association, Composition, generalization)}]{. UML Association (Aggregation, Association, Composition, generalization)}\par
There are some rules and requirements for combining the classes to construct partial or complete UML class models.\par
Association It can be depicted as bi-directional or unidirectional. The association lines indicate the possible relationship between the class entities \hyperref[b8]{[9]}. An association represents attributes and objects from the related classes, such as the relationship between class A and class C seenin Fig.  {\ref 1}. 
\section[{Figure 1: UML Class Diagram}]{Figure 1: UML Class Diagram}\par
Association ends can be annotated with labels, known as association end names and multiplicities. For example, multiplicity can be expressed as specific numbers, ranges of numbers, or unlimited numbers, as shown in Figure  {\ref 1 between classes A and C}. Aggregation An aggregation is represented as an association with a white diamond on one end, where the class at the diamond end is the aggregate (container class). It includes or owns instances of the class (contained class) at the other end of the association \hyperref[b8]{[9]} (e.g., the relationship between class A and B in Figure  {\ref 1}). Composition It is a special type of aggregation in which instances of the contained class are explicitly owned by instances of the container classes \hyperref[b8]{[9]}; if an instance of the container class is deleted, the instances of the contained class are also deleted. Figure  {\ref 1} shows class C, the container class, and class D, the contained class. It is represented as an association with a black diamond.\par
Generalization A generalization is represented by an association with a triangle on one end represents, where the class at the triangle end of the association is the parent class of the classes at the other ends of the association, called subclasses \hyperref[b8]{[9]}. A subclass inherits all of the parent class's attributes, operations, and associations (e.g., subclasses E and F inherit properties of parent class C in Figure  {\ref 1}). 
\section[{b) Model Transformation}]{b) Model Transformation}\par
Models provide a level of abstraction that allows developers and stakeholders to visualize different parts of the system while avoiding implementation details. A large number of models can exist for any given system, and it is essential to assure the consistency of those models \hyperref[b9]{[10]}.\par
Most software engineering operations have included model transformation in their development life cycle.\par
It is the process of transforming a graphical model for the purposes of analysis, optimization, evolution, migration, or even code generation. Model transformation employs a collection of rules known as transformation rules, which take one or more input models and output one or more target models \hyperref[b10]{[11]}.\par
Model transformation can be either manual or automatic. Manual transformation involves an application of custom transformation rules while in automatic transformation the predefined transformation rules are applied to class model \hyperref[b10]{[11]}. Regardless of the transformation method used, it is essential that the software engineer has a thorough understanding of the project's scope, as well as the syntax and semantics of the source and target models. Transformation rules will be designed and applied to the models in order to automate the transformation process. The source models will be UML class diagrams, and the target models will be their equivalent formal specification schemas. 
\section[{c) Formal Specification Methods}]{c) Formal Specification Methods}\par
The inadequacies of system and software specifications are one of the primary issues with software-intensive systems. Although the requirements should usually accurately describe the functions of the software system, many of the details that should be carried out and defined in a more detailed specification are not addressed.\par
As a result, there are inconsistencies and misinterpretations, which lead to issues in the latter stages of design and implementation. These issues are frequently identified during the system integration stages. There are graphical software development methods, such as data-flow diagrams, finite state machines, and entity relationship diagrams, that have been shown to help with the development of better specifications, but they lack precision in the details of the specification and a smooth way of developing a design and implementation.\par
Formal specification methods are feasible solution to these issues. They precisely define the system and ensure a smooth transition from specification to design to implementation. There are a number of formal specification languages such as Z notation, Object Constraint Language (OCL), VDM, Alloy etc. In general, all of these formal specification languages involve formal specification, refinement, and verification, which comprise of set theory, predicate logics, and algebra, among other things. The primary goal of our review is to compare two of these formal specification approaches i.e., Z notation and OCL.\par
The syntax and semantics of static and dynamic aspects of a system are formally specified in terms of mathematical notations in formal languages. Formal languages improve the system's reliability and security by reducing ambiguity in the system's requirements using their mathematical representation. The use of formal languages is essential while working with the large/complex real-time software systems in which the accuracy of the system is important.\par
The importance of formal languages increases in real-time safety critical systems where the primary concern is reliability and performance of the system. There is decent amount of work done in terms of defining and specifying formal languages for software systems and UML models, with some being accepted by the industry, such as Z, OCL, VDM, B, Alloy, etc. As each language has its own pros and cons, this survey compares two languages Z and OCL that can be utilize for verifying real-time safety critical systems. 
\section[{i. Z-notation}]{i. Z-notation}\par
The Z notation \hyperref[b11]{[12]}- \hyperref[b14]{[15]} is based on first-order logic and typed set theory. A schema i.e., a component of Z notation that describes the state and operations of a specification. A schema is a collection of variable declarations accompanied by a set of predicates that constrain the variable's possible values. 
\section[{ii. Object Constraint Language (OCL)}]{ii. Object Constraint Language (OCL)}\par
The Object Constraint Language (OCL) \hyperref[b15]{[16]}- \hyperref[b21]{[22]} is a constraint expression language for objectoriented languages and other modeling artifacts. OCL is a component of the Unified Modeling Language (UML) that plays a key role in the software lifecycle's analysis phase. For a detailed and unambiguous specification, traditional graphical models, such as class models, are insufficient. Therefore, We require to add some more constraints to the objects to resolve those issues. However, the classic formal method requires a significant knowledge of mathematics, making it difficult for the average business or system modeler to employ. OCL has been designed to bridge this gap. It was created by IBM's Insurance group as a business modeling language.\par
IV. 
\section[{Literature Review a) Z notation}]{Literature Review a) Z notation}\par
The Z notation is used in the first research [S1, \hyperref[b11]{[12]}\hyperref[b12]{[13]}\hyperref[b13]{[14]}\hyperref[b14]{[15]} to formalize and verify the UML class model. The authors  {\ref (Evans et al.)} employed Z notation to develop the formal foundation for the UML core meta model in S1. They claimed that the formal foundation provides a number of benefits, including transparency, extendability, consistency testing, refinement, and proof \hyperref[b11]{[12,}\hyperref[b12]{13]}.\par
They have defined a compositional schema with multiple subschema a as to represent the UML class model. The sub-schemas formalize UML model elements such as type, instance, values, operation, associations, generalization etc.\par
The authors also propose three alternatives for formalizing the UML model \hyperref[b11]{[12]}: 1) Supplementary: In this way, the UML model's informally specified elements are formally expressed. 2) Object-Oriented Extended Formal Language: In this approach, established formal methods are extended with object-oriented principles such as Object-Z and Z++. 3) Method Integration: In this method, the complete UML model is translated into a formal model in order to improve its precision.\par
The authors of \hyperref[b11]{[12]} expanded on their previous work by proposing a graphical representation transformation of the UML class model. They also offered a three-step roadmap for formalizing and verifying models: 1) Select a formal language that is both expressive and well supported by the tools for the model's static and dynamic features of UML class model. 2) Formally describe a graphical modeling notation's abstract syntax. 3) Define a function that transforms the model's syntax and semantics into formal notation. Finally, tools for validating formal semantics should be developed.\par
The authors of \hyperref[b13]{[14]} suggested that formal UML analysis alone is insufficient for determining semantic correctness. Furthermore, the authors stated that it is not particularly accessible to practitioners with limited knowledge of discrete mathematics, and that industry experts' comments is also necessary for the semantic validity of the UML model. In \hyperref[b14]{[15]}, Authors designed a formal methods reference manual for Z notation, which precisely and explicitly specifies the semantics of UML concepts. Along with that, the Inference rules for examining various UML model properties are provided in the reference manual \hyperref[b14]{[15]}. 
\section[{b) Object Constraint Language (OCL)}]{b) Object Constraint Language (OCL)}\par
In the second study [S2, \hyperref[b15]{[16]}\hyperref[b16]{[17]}\hyperref[b17]{[18]}\hyperref[b18]{[19]}\hyperref[b19]{[20]}\hyperref[b20]{[21]}\hyperref[b21]{[22]}, object constraints language (OCL) used for verification of the UML class model.\par
Cadoli et al. \hyperref[b15]{[16]} proposed a constraint programming-based linear inequality-based method for finite model verification. They used the Constraint Satisfaction Problem (CSP) to represent the UML class model, and the ILOG's Solver assessed the satisfiability of the UML class model \hyperref[b15]{[16]}. The Managed Object Format (MOF) syntax is used by the ILOG solver as an input. In addition, two class model correctness issues were addressed and encoded into CSP. In the first problem, they check that all the model's classes are completely satisfied at the same time. In the second problem, they prove that a finite non-empty model can be generated from the class model.\par
To verify the UML class model, Malgouyres and Motet \hyperref[b16]{[17]} employed Constraint Logic Programming (CLP). They used CLP clauses to translate the UML class model, metamodel, and meta-metamodel \hyperref[b16]{[17]}. In this approach, c Concrete metamodel and UML class model elements are translated into CLP facts while abstract elements and constraints are transformed into rules. CLP's goals are also specified, which contradicts the consistency standards. Finally, the inconsistencies are handled by a unified checker. The UML class model is considered inconsistent if the unified checker identifies the solution to the goal and if the goals are resolved.\par
Pérez and Porres \hyperref[b17]{[18]} proposed a system for using CLP to assess the satisfiability of a UML class model. The suggested methodology detects design flaws in UML class models with OCL annotations. They used the bounded verification approach and used the model-finding tool formula to reason about finite constraints for the number of instances of the model. The suggested method verifies predefined correctness features such as satisfiability and the lack of redundant constraints. It can also be used to analyze complex models in order to discover the optimal object model for the domain. They also used an eclipse plug-in called CD-to-Formula to design the proposed framework.\par
Cabot et al. \hyperref[b18]{[19]} presented incremental verification of the class model's OCL integrity constraint. Integrity checking is a technique used for determining whether an operation violates a specified integrity constraint. They introduced the term Potential Structure Event (PSE) and stated that verifying integrity requirements after each structure event (e.g., Insert, Update, Delete, or Specialized Entity) can be costly and time-consuming \hyperref[b18]{[19]}. As a result, PSEs for each integrity constraint are recorded, and only those events that can violate the constraint are represented. Furthermore, only the instances of entity and relationship types that have been affected by PSEs are validated and verified.\par
Cabot et al. \hyperref[b19]{[20]} presented an approach to translate UML class models annotated with OCL constraints into a constraint satisfaction problem (CSP). The authors briefly discussed translation of UML/OCL classes, associations, generalization sets, and OCL invariants into CSP. A tool based on CSP \hyperref[b20]{[21]} is then used to verify a predefined set of correctness properties for the original UML/OCL diagrams. The UML/OCL language combination integrates well with automated inference systems. If the generated CSP is solvable, the model is considered satisfiable otherwise is considered unsatisfiable. The CSP tool supports bounded reasoning about satisfiability, consistency, finite satisfiability, independence of invariants, and partial state completion. It handles class diagrams with multiplicity, class hierarchy, association-class constraints but does not allow multiple inheritance. Along with that, tool does not support all the features in OCL specification, such as constraints on a string, aggregation, and composition relationship.\par
Cabot et al. presented the UML to CSP tool in \hyperref[b20]{[21]}. It takes the XMI format for the class model and OCL as a separate text file for input. The model and OCL are translated to CSP, which is then verified by the CSP solver. The XMI file is parsed using the Metadata Repository API, while OCL constraints are processed by the Dresden OCL Toolkit.\par
Cabot et al. \hyperref[b21]{[22]} expanded on their previous work \hyperref[b19]{[20]}, arguing that an insufficient constraint or bound could miss defects in the model due to a small search space or could be inefficient if set too large. Large initial bounds and constraints are set in the proposed solution \hyperref[b21]{[22]}. Then, using the interval constraint propagation technique, the set of bounds is tightened up as much as feasible with user input, and unwanted value from the bounds is removed. Since then this technique has been enhanced to the point where verification bounds are now defined automatically whenever its possible. 
\section[{V. Review Summary and Conclusion}]{V. Review Summary and Conclusion}\par
Software design models play an important part in modern software development. They are useful for more than just documentation; they are also used for analysis, design, testing, and even code development using an automated transformation technique. The transformation technique allows existing software artifacts to be reused automatically. However, it has several flaws, such as the fact that model flaws are automatically transmitted to the changed model through the transformation. These flaws are difficult to detect and correct. Model verification appears to be a viable solution to the problem.\par
The verification of the UML class model is essential for assuring model quality prior to transformation. Verification of the UML class model through formal notation has been discussed in several studies. In this review, we discussed prior works in the field of formal specification specially related to Z and OCL methods. We presented a comparison of these formal methods in Table \hyperref[tab_2]{2} based on the analysis of studies \hyperref[b11]{[12]}- \hyperref[b21]{[22]}. This comparison is performed based on the features like support for UML features, Tool support, feedback for the user, and the efficiency of the methods and verification tool. Both the methods provide support for association, aggregation, and generalization relationships and do not support the features like dependency relationships (aggregation and composition) and x or constraint. Z notation is supported by Z word and Z/Eves verification tools. USE and UML to CSP tools are capable of working with OCL. Both of these tools support semi-automatic transformation. Both the tools (Z word and USE) provide feedback to users in order to notify them of the verification process's outcome. Z word provides the successful message in textual form on a pop-up window. In case of USE tool, if the verification process ends successfully it is complemented by a sample object model. This sample object model acts as the proof of the verification. When the verification process does not succeed, the Z Word and USE tools can display some hints in textual form on a window. This can help model designers in identifying the reasons for the failure and adjusting the model accordingly.\par
However, this models or tools require from the user a significant level of expertise on formal aspects in order to understand the feedbacks and resolve the issues. Overall, We can say that the existing verification tools, apart from being certainly limited in size, is in some cases targeted at a very limited or specific audience.\par
Finally, efficiency is a major concern. Current UML class model verification methods effectively verify the correctness of small models with few constraints. However, in some circumstances, especially when dealing with large and complex models, their performance suffers. Along with that, they also lack support for certain key features of the UML class model.\par
Unfortunately, none of the verification tools examined in this study performs well in terms of achieving the verification requirements. These tools and methods in general do not integrate well and have been developed to conduct verification apart from the rest of the activities that characterize a model designer's work. It forces users to switch between model editors and verification tools to check for errors every time models are refined or improved, usually with little or no hint on where to apply fixes if the verification fails.\par
To conclude this, in my opinion, a verification tool, in order to be effective and widely adopted, has to present, at least, few important characteristics: 1) It should provide support for some key features of UML class model (i.e., aggregation, composition, x or constraint), 2) It should easily integrate into the model designer tool chain, 3) It should offer meaningful feedback for the user, and 4) It should be relatively efficient while verifying the large or complex real-world UML class models.\begin{figure}[htbp]
\noindent\textbf{1} \par 
\begin{longtable}{P{0.85\textwidth}}
What is the importance of UML models and static\\
CD models?\\
RQ2: What is the importance of model transformation\\
and formal specification methods?\\
RQ3: Which model defects have been undertaken in\\
proposed approach?\\
RQ4: Is a verification approach supported by the tool?\\
RQ5: What are the deficiencies associated with the\\
selected formal approach?\end{longtable} \par
 
\caption{\label{tab_0}Table 1 :}\end{figure}
 \begin{figure}[htbp]
\noindent\textbf{2} \par 
\begin{longtable}{P{0.01706827309236948\textwidth}P{0.2577309236947791\textwidth}P{0.07339357429718876\textwidth}P{0.3072289156626506\textwidth}P{0.19457831325301203\textwidth}}
Method\tabcellsep Support for UML Features\tabcellsep Tool Support\tabcellsep Feedback to user\tabcellsep Efficiency\\
\tabcellsep \tabcellsep \tabcellsep Error: Does not provide\tabcellsep \\
Z\tabcellsep Association, Generalization, Multiplicity Constraints\tabcellsep Z Word, Z/Eves\tabcellsep meaningful feedback Successful: message in textual form on a pop-up\tabcellsep Not efficient with large or complex UML class models\\
\tabcellsep \tabcellsep \tabcellsep window\tabcellsep \\
OCL\tabcellsep Association, Association Classes, Generalization, Multiplicity Constraints\tabcellsep USE Tool UMLtoCSP\tabcellsep Error: Does not provide meaningful feedback Successful: object model\tabcellsep Not efficient with large or complex UML class models\end{longtable} \par
 
\caption{\label{tab_2}Table 2 :}\end{figure}
 		 		\backmatter  			  				\begin{bibitemlist}{1}
\bibitem[Spivey and Michael ()]{b14}\label{b14} 	 		\textit{},  		 			J Spivey 		,  		 			J R Michael 		.  	 	 		\textit{The Z notation}  		1992. Prentice Hall. 29.  	 
\bibitem[Gutwenger et al. (2003)]{b8}\label{b8} 	 		‘A New Approach For Visualizing UML Class Diagrams’.  		 			C Gutwenger 		,  		 			M Jünger 		,  		 			K Klein 		,  		 			J Kupke 		,  		 			S Leipert 		,  		 			P Mutzel 		.  	 	 		\textit{Proc ACM Symp. Software Visualization (SOFTVIS03)},  				 (ACM Symp. Software Visualization (SOFTVIS03))  		June 2003. Association for Computing Machinery. p. .  	 
\bibitem[Davis et al. ()]{b0}\label{b0} 	 		‘A strategy for comparing alternative software development life cycle models’.  		 			Alan M Davis 		,  		 			H Edward 		,  		 			Edward R Bersoff 		,  		 			Comer 		.  	 	 		\textit{IEEE Transactions on software Engineering}  		1988. 14  (10)  p. .  	 
\bibitem[Malgouyres and Motet ()]{b16}\label{b16} 	 		‘A UML model consistency verification approach based on meta-modeling formalization’.  		 			Hugues Malgouyres 		,  		 			Gilles Motet 		.  	 	 		\textit{Proceedings of the 2006 ACM symposium on Applied computing},  				 (the 2006 ACM symposium on Applied computing)  		2006. p. .  	 
\bibitem[Meedeniya and Apeksha ()]{b3}\label{b3} 	 		\textit{Correct model-tomodel transformation for formal verification},  		 			Dulani Meedeniya 		,  		 			Apeksha 		.  		2013.  		 			University of St Andrews 		 	 	 (PhD diss) 
\bibitem[Mens and Van Gorp ()]{b2}\label{b2} 	 		\textit{Electronic notes in theoretical computer science},  		 			Tom Mens 		,  		 			Pieter Van Gorp 		.  		2006. 152 p. .  	 	 (A taxonomy of model transformation) 
\bibitem[Cadoli et al. ()]{b15}\label{b15} 	 		‘Finite satisfiability of UML class diagrams by Constraint Programming’.  		 			Marco Cadoli 		,  		 			Diego Calvanese 		,  		 			Giuseppe De Giacomo 		,  		 			Toni Mancini 		.  	 	 		\textit{CSP Techniques with Immediate Application (CSPIA)}  		2004. 2 p. .  	 
\bibitem[Clark and Evans (1997)]{b13}\label{b13} 	 		‘Foundations of the unified modeling language’.  		 			T Clark 		,  		 			A Evans 		.  	 	 		\textit{Proc. 2nd Northern Formal Methods Workshop},  				 (2nd Northern Formal Methods WorkshopIlkley, U.K.)  		Jul. 1997. Springer. p. .  	 
\bibitem[Dobing and Parsons ()]{b5}\label{b5} 	 		‘How UML is used’.  		 			Brian Dobing 		,  		 			Jeffrey Parsons 		.  	 	 		\textit{Communications of the ACM}  		2006. 49  (5)  p. .  	 
\bibitem[Cabot and Teniente ()]{b18}\label{b18} 	 		‘Incremental evaluation of OCL constraints’.  		 			Jordi Cabot 		,  		 			Ernest Teniente 		.  	 	 		\textit{International Conference on Advanced Information Systems Engineering},  				 (Berlin, Heidelberg)  		2006. Springer. p. .  	 
\bibitem[Varró ()]{b9}\label{b9} 	 		‘Model transformation by example’.  		 			Dániel Varró 		.  	 	 		\textit{International Conference on Model Driven Engineering Languages and Systems},  				 (Berlin, Heidelberg)  		2006. Springer. p. .  	 
\bibitem[Sendall and Kozaczynski ()]{b10}\label{b10} 	 		‘Model transformation: The heart and soul of model-driven software development’.  		 			Shane Sendall 		,  		 			Wojtek Kozaczynski 		.  	 	 		\textit{IEEE software}  		2003. 20  (5)  p. .  	 
\bibitem[Pérez and Porres ()]{b17}\label{b17} 	 		‘Reasoning about UML/OCL class diagrams using constraint logic programming and formula’.  		 			Beatriz Pérez 		,  		 			Ivan Porres 		.  	 	 		\textit{Information Systems}  		2019. 81 p. .  	 
\bibitem[Evans ()]{b12}\label{b12} 	 		‘Reasoning with UML class diagrams’.  		 			Andy S Evans 		.  	 	 		\textit{Proceedings. 2nd IEEE Workshop on Industrial Strength Formal Specification Techniques},  				 (2nd IEEE Workshop on Industrial Strength Formal Specification Techniques)  		1998. IEEE. p. .  	 
\bibitem[Lano et al. ()]{b7}\label{b7} 	 		‘The UML as a Formal Modeling Notation’.  		 			A Lano 		,  		 			R Evans 		,  		 			K France 		,  		 			B Rumpe 		.  	 	 		\textit{Computer Standards and Interfaces}  		1998. 19 p. .  	 
\bibitem[France et al. ()]{b11}\label{b11} 	 		‘The UML as a formal modeling notation’.  		 			Robert France 		,  		 			Andy Evans 		,  		 			Kevin Lano 		,  		 			Bernhard Rumpe 		.  	 	 		\textit{Computer Standards \& Interfaces}  		1998. 19  (7)  p. .  	 
\bibitem[Rumbaugh et al. ()]{b6}\label{b6} 	 		\textit{The Unified Modeling Language Reference Manual},  		 			J Rumbaugh 		,  		 			I Jacobson 		,  		 			G Booch 		.  		2004. Hoboken, NJ, USA: Pearson Higher Education.  	 
\bibitem[Booch et al. ()]{b1}\label{b1} 	 		\textit{The Unified Modeling Language, Rational Software Corporation},  		 			G Booch 		,  		 			J Rumbaugh 		,  		 			I Jacobson 		.  		1997. Addison-Wesley, Indiana, USA.  	 
\bibitem[Clarisó et al. ()]{b21}\label{b21} 	 		‘Towards domain refinement for UML/OCL bounded verification’.  		 			Clarisó 		,  		 			Carlos A Robert 		,  		 			Jordi González 		,  		 			Cabot 		.  	 	 		\textit{SEFM 2015 Collocated Workshops},  				 (Cham)  		2015. Springer. p. .  	 
\bibitem[Cabot et al. ()]{b20}\label{b20} 	 		‘UMLtoCSP: a tool for the formal verification of UML/OCL models using constraint programming’.  		 			Jordi Cabot 		,  		 			Robert Clarisó 		,  		 			Daniel Riera 		.  	 	 		\textit{Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering},  				 (the twenty-second IEEE/ACM international conference on Automated software engineering)  		2007. p. .  	 
\bibitem[Unified Modeling Language Specification. Version 2.5 (2012)]{b4}\label{b4} 	 		\textit{Unified Modeling Language Specification. Version 2.5},  		October 2012.  		 			Object Modeling Group 		 	 
\bibitem[Cabot et al. ()]{b19}\label{b19} 	 		‘Verification of UML/OCL class diagrams using constraint programming’.  		 			Jordi Cabot 		,  		 			Robert Claris 		,  		 			Daniel Riera 		.  	 	 		\textit{2008 IEEE International Conference on Software Testing Verification and Validation Workshop},  				2008. IEEE. p. .  	 
\end{bibitemlist}
 			 		 	 
\end{document}
