I nte rna t io na l J o urna l o f   E lect rica l a nd   Co m p ute r  E ng in ee ring   ( I J E CE )   Vo l.   9 ,   No .   4 ,  A u g u s t   201 9 ,   p p .   3 0 6 9 ~ 3 0 7 6   I SS N:  2088 - 8708 ,  DOI : 1 0 . 1 1 5 9 1 / i j ec e . v 9 i 4 . p p 3 0 6 9 - 3076           3069       J o ur na l ho m ep a g e :  h ttp : //ia e s co r e . co m/ jo u r n a ls /in d ex . p h p / I JE C E   An  int eg ra tion   o f  u m l  use cas e  dia g ra m   a nd   a ctivity   dia g ra m   w ith  Z   la ng ua g e f o r  for m a li z a t io n  o f  libra ry     m a na g e m ent  sy ste m       Z a i na b H a s s a n M uh a m a d 1 ,   Dha f er   Abdu la m ee r  A bd ul m o n i m 2 ,  B a s ha r  Ala t ha ri 3   1, 2   Dep ar tm en t o f   C o m p u ter   Sc ien ce ,  Dir ec to r ate  o f   E d u ca ti on   in   Naj af ,  I r aq i M in is tr y   o f   E d u ca tio n ,   I r aq   3 I T R DC ,   Un iv er s it y   o f   K u f a ,   I r aq       Art icle  I nfo     AB ST RAC T   A r ticle  his to r y:   R ec eiv ed   J u n   2 8 ,   2 0 1 8   R ev i s ed   Mar   2 2 ,   2 0 1 9   A cc ep ted   A p r   3 ,   2 0 1 9       Un if ied   M o d e li n g   L a n g u a g e   ( U M L )  is  th e   e ffe c ti v e   sta n d a rd   f o r  m o d e li n g   o b jec t - o rie n ted   so f tw a re   s y ste m s.  Ho w e v e r,   th e   a m b ig u it y   o f   se m a n ti c s  a n d   th e   a b se n c e   o f   c o n siste n c y   a m o n g   UML   d iag ra m s  lea d   to   lac k   o f   p re c ise l y   d e f in in g   th e   re q u irem e n ts o f   a   s y s tem .   On   th e   o th e r  h a n d ,   f o rm a l  m e th o d s a re   tec h n iq u e s  a n d   to o ls  u se   th e   m a th e m a ti c a l  n o tatio n s ,   a n d   th e y   i n v o lv e   th e   p re c ise   s y n tax   a n d   se m a n ti c s  o f   th e   u n a m b ig u o u s  so f twa re   r e q u irem e n ts  sp e c if ic a ti o n .   It   a p p li e d   in   e a rl y   s tag e s   o f  S o f t w a re   De v e lo p m e n t  L i f e   C y c l e   (S DL C).   T h e re f o re ,   a n   in teg ra ted   b e tw e e n   UML   sp e c i f ica ti o n   a n d   f o rm a l   sp e c if ic a ti o n   is  re q u ired   t o   re d u c e   th e   re q u irem e n ts'   a m b ig u it y   a n d   e rro r,   a n d   to   im p ro v e   th e   q u a li ty   a n d   se c u rit y   o f  so f t wa re   s y ste m s.  T h is  p a p e r  p ro p o se s  a n   a p p r o a c h   i n v o lv e s  th e   c o m b in in g   UML   u se - c a se   d iag ra m   a n d   a c ti v it y   d iag ra m s  w it h   Z  lan g u a g e   f o r  f o r m a li z a ti o n   o f   L ib ra r y   M a n a g e m e n t  S y ste m   (L M S ).   T h e   f o c u s  o f   th is   p a p e r  is  o n   c o n siste n c y   b e twe e n   th e   UM L   d iag ra m s   to   Z  S c h e m a ,   a n d   th e n   v e rif ied   b y   u sin g   t h e   Z  /  EVEs  to o l.     K ey w o r d s :   Fo r m al  m e th o d   Fo r m al  s p ec i f icatio n   Un i f ied   m o d eli n g   la n g u a g e   Z   l a n g u a g e   Co p y rig h t  ©   2 0 1 9   In stit u te o f  A d v a n c e d   E n g i n e e rin g   a n d   S c ien c e .    Al l  rig h ts re se rv e d .   C o r r e s p o nd ing   A uth o r :   Dh a f er   A b d u la m ee r   A b d u l m o n i m ,    Dep ar t m en t o f   C o m p u ter   Scie n ce ,   Dir ec to r ate  o f   E d u ca tio n ,   I r aq i M in is tr y   o f   E d u ca t io n ,   Naj af ,   I r aq .   E m ail:  D h a f er 9 8 5 @ g m a il . c o m       1.   I NT RO D UCT I O N     Un i f ied   Mo d elin g   L an g u ag e  ( UM L )   i s   a  v i s u al  la n g u a g e  f o r   co n s tr u cti n g   an d   m o d elin g   o f   s o f t w ar e   s y s te m s .   I t   co m b i n es   a  g r ap h i ca l  n o tatio n   w i th   a  s e m i - f o r m al  lan g u ag e   f o r   o b j ec t - o r ien ted   b ased   s y s te m ,   to   p r o v id e  r eq u ir em e n t s   s p ec i f i ca tio n s   w i th   s y n ta x   a n d   s e m an tics   co n s tr ai n ts   [ 1 ,   2 ] .   UM L   d ia g r a m s   ar e   co n s id er ed   as  a  s ta n d ar d   to o l  to   co m p o s e  r eq u ir e m en t s ,   a n d   th e n   tr a n s f o r m   th e m   in to   s tr u ctu r es.  I n   o r d er   to ,   u n d er s ta n d   s y s te m 's   r eq u ir e m en ts   a n d   r ed u ce   co m p lex it y   o f   th e  s y s te m .   UM L   in cl u d es   th ir teen   d ia g r a m s :   Use  C ase,   C la s s ,   A cti v it y   a n d   o th er s .   Ho w e v er ,   th er e  is   th e  lack   o f   p r ec is io n   in   t h e  d ef i n itio n   o f   UM L   n o tatio n s   an d   s e m an tic s   [ 3 ] .   C o n s eq u en tl y ,   UM L   d iag r a m s   h av e  a  d if f er e n t  in ter p r etati o n   o f   th e  d escr ib ed   m o d el.   I n   ad d itio n   to ,   t h e  co n s is te n c y   b et w ee n   m o d el s   is   v e r y   cr itic al .   T h er ef o r e,   a  co n s i s ten c y   an d   a   co n ci s e   f o r m aliza t io n   o f   UM L   s e m an tics   i s   r eq u ir ed   f o r   m ap p in g   b et w ee n   g r ap h ical  an d   lo g ical  b y   u s i n g   m at h e m a tical  th eo r ies  [ 4 ].   I n   So f t w ar e  E n g i n ee r in g ,   th e  in te g r ated   f o r m al  s p ec i f i ca tio n s   an d   UM L   s p ec if icatio n s   ar e  v er y   u s ef u l  to   u n d er s ta n d   th e  r eq u ir e m en t s   s p ec if ica tio n s   o f   an y   s y s te m   b y   co m b i n atio n   o f   UM L   d ia g r a m s   w it h   f o r m al  ap p r o ac h es  [ 5 ,   6 ] .   W ith   e m p h asi s   o n   c o n s is ten c y   b et w ee n   UM L   d iag r a m s .  Fo r m al  m et h o d s   ar e  tech n iq u es  b ased   o n   m at h e m atica l  n o t atio n s ,   w h ich   p la y   a  cr itical  r o le  as  th e y   f o c u s   o n   r ef in e m e n t  o f   r eq u ir e m e n ts   i n   th e  i n itia l  s ta g es  o f   t h e  S y s te m   De v elo p m e n t  L i f e  C y cl e  ( SDLC)  lik e  t h e   r eq u ir e m en ts   an al y s is   a n d   s p ec if icatio n .   I t  u s ed   to   en s u r e  t h at  t h e   r eq u ir e m e n t s   s p ec i f ica tio n s   ar e  p r ec is el y   ex p r ess .   I n   o r d er   to   r ef in e m e n t  o f   a  s y s te m 's  r eq u ir e m en t s   w h ic h   th er e f o r e  in cr ea s e  t h e   s y s te m ’ s   ac cu r ac y   Evaluation Warning : The document was created with Spire.PDF for Python.
                      I SS N :   2 0 8 8 - 8708   I n t J   E lec  &   C o m p   E n g ,   Vo l.  9 ,   No .   4 ,  A u g u s t   201 9   :   3 0 6 9   -   3 0 7 6   3070   an d   co n s is te n cy   [ 7 ] .   Fo r m al  m et h o d s   s p ec if y   t h e  u n a m b i g u o u s   s y s te m   s p ec i f icatio n ,   r ed u ce   th e  er r o r   an d   i m p r o v ed   ef f ec ti v e n ess   in   d esig n   a n d   d ev elo p m e n t  p h a s es  [ 8 ,   9 ] .   T h e  f o r m al  s p e cif icatio n   r e m o v es   a m b ig u it y ,   r ed u ce s   th e  d esi g n   ti m e,   it  also   ad d r ess es  i m p r o v e  s o f t w ar e ' s   r e liab ilit y   a n d   co m p r eh en s ib ilit y   [ 10 ] .   Fo r m al  s p ec i f icatio n   l an g u a g es  ar e  w id el y   u s ed   f o r   d ev elo p m e n t  a n   ac c u r at e,   co n s is ten t   an d   u n a m b i g u o u s   s y s te m s   an d   s o f t w ar e .  O n   t h at  p o in t  ar e  v a r io u s   f o r m al  la n g u a g e s   li k e  VDM ,   B - Me t h o d s ,   L ar ch   a n d   Z   n o tatio n   ar e  u s ed   f o r   f o r m a l  s p ec if ica tio n .   Z   n o tatio n   is   a  g o o d   ex a m p l e  b ased   o n   f o r m a l   s p ec if icatio n   lan g u ag e  w h ich   u s es  t h e  s et  th eo r y   f o r   d eter m i n in g   t h e  b eh av io r   o f   s eq u e n tial  s y s te m s   [ 1 1 ] .   T h e  liter atu r e  i n d icate s   t h at  th e  m o s t   w ell - k n o w n   is s u e  f o r   UM L   is   lack   o f   o b v io u s   s e m a n tic s ,   v ar io u s   in ter p r etatio n   o f   t h e  d ia g r a m   a n d   i n co n s i s te n c y   a m o n g   d iag r a m s .   T h i s   lead s   to   a m b i g u it y ,   er r o r s ,   an d   r ed u ce d   s o f t w ar e  q u ali t y .   i n   ad d itio n ,   t h e  m o s t  p o p u lar   UM L   d ia g r am s   u s ed   i n   in d u s tr y   ar e  u s e  c ase,   class ,   s eq u en c e   to   in teg r ate  w i th   f o r m al  m et h o d s .   B u t,  T h e  f o r m al  s p ec if ic atio n s   h av e  n o t  b ee n   m ad e  f r o m   ac ti v it y   d iag r a m .   Hen ce ,   t h e  co m b in a tio n   o f   in f o r m al   m e th o d   a n d   f o r m al   m eth o d   is   r eq u ir ed   to   h a n d le  a m b ig u it y ,   s p ec if y i n g   co n s is ten c y   a n d   i m p r o v i n g   co m p lete n e s s   [ 1 2 ] .   T h er ef o r e ,   th is   p ap er   p r o p o s es  an   ap p r o ac h   th at  ai m s   to   in te g r ate  o f   UM L   u s e   ca s e   an d   ac tiv it y   d ia g r a m s   w i th   f o r m al  s p ec i f icatio n   m e th o d ,   to   b r i d g e  a  g ap   b et w ee n   in f o r m al  a n d   f o r m al  m et h o d s .   T h e  m ai n   f o cu s   o f   t h is   p ap er   is   o n   co n s is te n c y   a n d   co m p le m en t  a m o n g   UM L   us e  ca s e  d iag r a m ,   UM L   ac ti v it y   d ia g r a m   an d   Z   s ch e m as .   B esid es,  th er e  w a s   a  r esear ch   g ap   o f   p r o p e r   in te g r atio n   o f   ac ti v it y   d iag r a m s   w ith   f o r m al  s p ec if ica tio n s .   A l s o ,   Z   n o tatio n   u s ed   f o r   f o r m al  an a l y s is   o f   L MS   ( L MS)   w h ich   i s   f u r t h er   v er i f ie d   b y   u s i n g   t h e  Z /EV E S to o l.     T h e  r est  o f   th i s   p ap er   o r g an iz ed   as  f o llo w s .   Sect io n   2   i n tr o d u ce s   t h e  r elate d   w o r k .   Secti o n   3   f u ll y   d escr ib es  th e  p r o p o s ed   ap p r o ac h   to   in te g r ate  o f   UM L   u s e  ca s e  a n d   ac ti v it y   d iag r a m s   w it h   f o r m a l   s p ec if icatio n   m e th o d .     Sectio n   4   p r esen ts   th e  r es u lt s   o f   t h e  c ase  s t u d y   to   d e m o n s tr ate  th e  e f f ec tiv e n e s s   o f   t h e   p r o p o s ed   ap p r o ac h .     Sectio n   5   d escr ib es  th e  s tr en g t h   an d   w ea k n ess   o f   th e  p r o p o s ed   ap p r o ac h .   an d   f in all y   Sectio n   6   r e m ar k s   th e  co n clu s i o n s .       2.   RE L AT E D  WO RK S   T h e  f o r m al  ap p r o ac h   f o r   r eq u ir e m e n t s   s p ec i f icatio n   u s i n g   Z   la n g u a g e  t h at  h ad   b ee n   ad d r ess ed   b y   m an y   r esear c h er s   [ 4 ,   6 – 8 ,   1 1 ,   1 2 ] ,   th ey   w er e  o f f er ed   it  in   d if f er en t  a s p ec ts .   T h e  s o lu tio n   h as  p r o d u ce d   w it h   g r ea ter   i m p r o v e m e n t  t h an   i n f o r m al  m et h o d .   Min h as,  et  al.   [ 4 ]   p r o p o s ed   an   in teg r atio n   o f   UM L   s p ec if ica tio n   w it h   f o r m al  s p ec if icat io n .   T h e y   h av e   b ee n   u s ed   UM L   s e q u en ce   d ia g r a m   a n d   Z   la n g u ag e  f o r   d ev elo p ed .   T h e  Fli g h t  R e s er v atio n   S y s te m .   I n   ad d itio n ,   t h e y   co n clu d e d   to   u s e  m o r e  th a n   o n e  U ML   d iag r a m ,   i n   o r d er   to   th e  r es u lts   ca n   b e  m o r e  i m p r o v ed .   T o   c o v er   am b ig u it y ,   id en tify i n g   co n s i s ten c y   a n d   en h a n cin g   co m p lete n es s ,   th e  i n f o r m al  an d   f o r m al  m et h o d   co m b in at io n   is   p r o p er   to   d ev elo p   th e  R o ad   T r af f ic  Ma n ag e m e n t  S y s te m   b y   Sin g h ,   et  al.   [ 6 ] .   I n   th eir   s tu d y   UM L   u s e  ca s e,   class   a n d   s eq u en ce   d iag r a m s   w i th   Z   lan g u a g e  u s ed .   Mo r eo v er ,   th e  Z /E VE s   to o l  u s ed   to   v er if y   Z   s c h e m a s .   I n   th e  r esear ch   p r o v id ed   f r o m   B ak r i  et  al.   [ 7 ] ,   r elate d   to   o u r   r esear ch   s tu d y   w h er e  t h e y   o f f er   a   f o r m al   s p ec i f icatio n   f o r   t h e  in v e n to r y   s y s te m   u s i n g   Z   lan g u ag e.   T h eir   ap p r o ac h   b ased   o n   tr an s la tin g   t h e  UM L   s p ec i f icatio n   i n to   Z   s c h e m a s .   I t a ls o   f o cu s ed   o n   th e  co n s i s ten c y   b et w ee n   UM L   s p ec if icatio n   an d   Z   s c h e m a,   i n   o r d er   to   ef f ec tiv e l y   i m p r o v e   s y s te m   r el iab ilit y   a n d   r ed u c e   d ef ec t  f o r   d ev elo p in g   t h e  i n v en to r y   s y s te m .   Ho w e v er ,   in   t h eir   s t u d y   h a v e  b ee n   u s ed   U ML   cla s s   d iag r a m .   R esear ch er s   p r esen ted   i n   [ 8 ,   1 1 ,   1 2 ]   f o r m al  s p ec if ica tio n s   b y   u s i n g   UM L   u s e  ca s e  d iag r a m   a n d   Z   s c h e m as  t o   i m p r o v e  s o f t w ar e  co r r ec tn es s ,   r eliab ilit y ,   a n d   ef f icie n c y .   A s   it  u s ed   to   r ed u ce   ti m e  an d   co s t   at  an   i n itia l  s ta g e.   Ho w e v er ,   in   [ 8 ]   h av e  b ee n   u s ed   Z /EV E s   to o l  to   v er i f y   Z   s c h e m a s .   W h i le,   in   b o th   o f   th e   s tu d ie s   [ 1 1 ,   1 2 ]   n o   to o l   u s ed   to   v er i f y   Z   s c h e m as.  T h e  co m p ar ativ e  s tu d y   o f   r elate d   w o r k s   f o c u s ed   o n   a   n u m b er   o f   f o r m a l   s p ec if icatio n   ap p r o ac h es to   i m p r o v e  th e  s y s te m s   d ev elo p m e n t   as r ev ie w ed   in   T ab le  1 .       T ab le  1 .   R ev ie w   o f   r elate d   w o r k s   A u t h o r   n a me /   y e a r   A   P r o p o s e d   A p p r o a c h   T h e   r e su l t s o b t a i n e d   f r o m t h e   c o mb i n a t i o n   o f   i n f o r mal   a n d   f o r mal   sp e c i f i c a t i o n   S u p p o r t e d   U M L   d i a g r a ms   F o r mal   M e t h o d   V e r i f i c a t i o n   S .   H .   B a k r i ,   e t   a l .   2 0 1 3   [ 7 ]   U se   c a se ,   C l a ss   Z   l a n g u a g e   Z / EV Es  t o o l   I mp r o v e   t h e   sy st e m q u a l i t y   a n d   r e d u c e   c o st   M .   W .   A z e e m ,  e t   a l .   2 0 1 4   [ 1 1 ]   U se   c a se   Z   l a n g u a g e   _ _ _   I mp r o v e   t h e   q u a l i t y   e f f i c i e n t l y ,   f i x i n g   b u g s a n d   r e d u c e   t i me   a n d   c o st   N .   M .   M i n h a s,   e t   a l .   2 0 1 5   [ 4 ]   S e q u e n c e   Z   l a n g u a g e   F u z z   t o o l   T h e   i n t e g r a t i n g   o f   se q u e n c e   a n d   o t h e r   U M L   d i a g r a m i s   mo r e   e f f e c t i v e   S .   A .   K h a n   &   H .   Ja msh e d ,  2 0 1 6   [ 1 2 ]   U se   c a se   Z   l a n g u a g e   _ _ _   I mp r o v e   c o r r e c t n e ss,  r e l i a b i l i t y ,   u se r   f r i e n d l i n e ss  a n d   e f f i c i e n c y .   M .   S i n g h ,  e t   a l .   2 0 1 6   [ 6 ]   U se   c a se ,   C l a ss,   S e q u e n c e   Z   l a n g u a g e   Z / EV Es  t o o l   U n a m b i g u i t y ,   c o n si s t e n c y   a n d   c o mp l e t e n e ss    P .   S a r a t h a ,  e t   a l .   2 0 1 7   [ 8 ]   U se   c a se   Z   l a n g u a g e   Z / EV Es  t o o l   U n a m b i g u o u s sy st e m sp e c i f i c a t i o n ,   r e d u c e   t h e   e r r o r   a n d   i m p r o v e d   e f f e c t i v e n e ss   Evaluation Warning : The document was created with Spire.PDF for Python.
I n t J   E lec  &   C o m p   E n g     I SS N:  2088 - 8708       A n   in teg r a tio n   o f u ml  u s e  ca s e   d ia g r a m  a n d   a ctivity  d ia g r a m  w ith   Z  la n g u a g e…     ( Za in a b   H a s s a n   Mu h a ma d )   3071   B ased   o n   T a b le  1 ,   th e  liter atu r e  in d icate s   th a t  th e  m o s t  p o p u lar   UM L   d iag r a m s   u s ed   in   i n d u s tr y   ar e   u s e  ca s e,   class ,   s eq u e n ce .   T h e  f o r m al  s p ec i f icatio n s   d id   n o t  co n s tr u ct  f r o m   ac ti v it y   d iag r a m   a s   w ell.   T h er ef o r e,   th is   p ap er   is   u s ed   c o m b i n atio n   o f   UM L   u s e  ca s e  an d   ac tiv i t y   d ia g r a m   w i th   Z   f o r m al  s p ec if ica tio n   lan g u a g e  to   d esig n   t h e  L M S.  I n   ad d itio n   to ,   w e  h av e  d is c u s s ed   ea r lier   th at  th e  m o s t  well - k n o w n   is s u e  f o r   UM L   is   lack   o f   clea r   s e m an t ics,  d if f er en t  i n ter p r etatio n   o f   th e  d escr ib ed   m o d el  an d   i n c o n s is ten c y   a m o n g   m o d el s .   Hen ce ,   t h e  co n s i s te n c y   b et w ee n   UM L   d ia g r a m s   an d   Z   s c h e m a   f o cu s ed   in   t h is   p ap er .       3.   RE SU L T S  A ND  AN AL Y SI S     UM L   i s   a  co m m o n   m o d elli n g   m e th o d   in   a n   o b j ec t - o r ien t ed   b ased   s y s te m .   T h e  co n s i s ten c y   is   a  s ig n i f ica n t  r u le  b et w ee n   d iag r a m s ,   to   en s u r e  th at  i m p le m en tatio n   o f   th e  d ia g r a m s   is   co m p le m en t in g .   Mo r eo v er ,   th e  co n s is te n c y   b et w ee n   u s e - ca s e  d iag r a m   an d   ac tiv it y   d iag r a m   co n f ir m ed   b y   [ 1 3 , 1 4 ] .     On   t h e  o t h er   h an d ,   Fo r m al  m e th o d s   ar e  a n   es s en tial  s o lu tio n   to   th e   is s u e s   r elate d   to   r eq u ir e m en t  a n al y s is   an d   s p ec if icatio n s .   I n   ad d itio n ,   it   d escr ib es  o f   u n a m b ig u it y   r e q u ir e m e n ts   s p ec i f icatio n s ,   a n d   en s u r es  th at   t h e   s y s te m   in d ee d   s ati s f ies  t h e  r eq u ir e m e n ts ,   r eliab ili t y   a n d   co r r ec ts   [ 1 0 ] .   C o n s eq u e n tl y ,   th is   p ap er   ai m s   to   p r o p o s e  an   ap p r o ac h   th at  i n te g r ates  UM L   d ia g r a m s   ( u s e  ca s e  d iag r a m   an d   ac ti v it y   d iag r a m )   w it h   t h e  f o r m al   s p ec if icatio n   la n g u a g e  ( Z   la n g u a g e)   f o r   s p ec i f y i n g   r eq u i r e m en t s   f o r   L MS,   a n d   t h en   v er if ied   b y   u s i n g   Z /EV E S  t y p e  ch ec k er   to o l.  T h is   to o l  u s ed   f o r   v er if y i n g   th e  s c h e m a  s p ec if ica tio n ,   th a t  w r o te  b ased   o n   Z   n o tatio n   la n g u a g e  [ 7 ] .   T h is   v er if ica tio n   i n cl u d es  s y n ta x   an d   s e m an t ics  o f   th e   L MS  f o r m al  s p ec if icatio n .     T h e  p r o p o s ed   a p p r o a ch   f o r   d esig n i n g   L M S u s es UM L   a n d   th e  f o r m a l  m et h o d   as s h o w n   i n   Fig u r e  1 .           Fig u r e  1 .   T h e  p r o p o s ed   a p p r o ac h   s tep s   to   in teg r ate  UM L   s p ec if ic atio n   w it h   f o r m a l sp ec if i ca tio n       4.   CASE   S T UD Y  AND  AP P R O ACH   M O DE L L I N G   I n   th is   p ap er ,   w e  p r esen t  a  ca s e  s tu d y   o f   A   L ib r ar y   Ma n ag e m en t  S y s te m   ( L MS) .   A   d ev el o p er   w an ts   to   d ev elo p   L MS.   W h e n   a  u s er   w a n ts   to   b o r r o w   a  b o o k ,   t h e  s y s te m   s h o u ld   b e  ab le  to   v er if y   th e  m e m b er s h ip   o f  th e  u s er   f ir s t,  if   t h e  u s er   is   a   m e m b er ,   th e n   t h e  s y s te m   c h ec k s   t h e  av ai lab ilit y   o f   t h e  b o o k .   I f   th e  b o o k   is   av ailab le,   th e n   th e  s y s te m   lets   th e  m e m b er   r eser v es  t h e  b o o k   an d   th e  d atab ase  n ee d s   to   u p d ate  to   in d icate   th at   th e  b o o k   is   n o t  av a ilab le  an y m o r e.   T h e  f ir s t  s tep   is   to   d eter m i n e  t h e  r eq u ir e m e n t s   an al y s i s   f o r   t h e  s ce n ar io   as   in   th e  n e x t s u b s ec tio n .     4 . 1 .     Sy s t em   re q uire m e nts a na ly s is     T h e  an al y s is   s tag e  w as  t h e  b asis   o f   th e  s y s te m   d esi g n .   At   th is   s ta g e,   it  n ee d s   to   o b tain   t h e  u s er   r eq u ir e m en ts   as  ac c u r ate,   a n d   an al y s i s   o f   d e m an d ,   t h u s   to   s p ec if y   s y s te m   r eq u ir e m en ts .   T h e  s y s te m   r eq u ir e m en ts   a n al y s is   i s   as  f o llo w s :   T h e  L MS   en tr u s ted   b y   b o o k   b o r r o w i n g   an d   b o o k   r etu r n   b u s in es s .   B o o k   b o r r o w s   m an a g e m en t  n ee d   to   v er if y   th e  m e m b er s h ip   o f   t h e  u s er   a n d   ch ec k   th e   av ai lab ilit y   o f   th e   b o o k .   A s   b o o k   r etu r n   m an a g e m en t  n ee d   to   v er i f y   th e  m e m b er s h ip   o f   t h e  u s er   an d   th e   leg a lit y   o f   t h e  b o o k .   L ib r ar ian   tas k   w as   to   m ain t ain   t h e  n e w   b o o k   in f o r m atio n   ad d itio n .   T h e  s t ak eh o ld er s   o f   th e  s y s te m   ar e   L ib r ar ian   a n d   Me m b er .   T h e  s y s te m   h a s   b asic   f u n ctio n s   t h at  ar e  Ver if y   m e m b er s h ip ,   C h ec k   a  b o o k   a v ailab ilit y ,   B o r r o w   a  b o o k ,   R etu r n   a  b o o k   a n d     A d d   a  b o o k .   Evaluation Warning : The document was created with Spire.PDF for Python.
                      I SS N :   2 0 8 8 - 8708   I n t J   E lec  &   C o m p   E n g ,   Vo l.  9 ,   No .   4 ,  A u g u s t   201 9   :   3 0 6 9   -   3 0 7 6   3072   4 . 2 .     Sy s t em   de s ig n ba s e d o n UM L   s pecif ica t io ns   B ased   o n   th e  ab o v e  an al y s i s ,   w e  t h en   d r a w   t h e  d iag r a m s   o f   UM L   m ain l y   t h e  u s e  ca s e  d i ag r a m   a n d   ac tiv it y   d iag r a m .   I n   th i s   p ap e r ,   th e  R atio n al  R o s e  UM L   to o l   u s ed   to   cr ea te  a   co m p le te  UM L   d iag r a m s .     Fig u r e  2   s h o w s   u s e  ca s e  d iag r a m   f o r   t h e  L M S.  T h er e  ar e  t w o   u s er s   to   u s e  t h e  s y s te m ,   w h i ch   ar e  L ib r ar ian   a n d   Me m b er .   A   L ib r ar ian   ca n   d o   ac tiv i tie s   f o r   B o r r o w   a  b o o k ,   R etu r n   a  b o o k   a n d   A d d   a  b o o k .   A s   a  Me m b er   ca n   d o   ac tiv ities   f o r   B o r r o w   a  b o o k   an d   R et u r n   a   b o o k .   W h ile ,   th e  f u n ct io n s   Ver if y   m e m b e r s h ip   a n d   C h ec k   a  b o o k ' s   av ailab il it y   ar e  i n cl u d ed   f u n ctio n s   o f   th e   s y s te m .   B as ed   o n   t h e  u s e  ca s e  d ia g r a m   in   Fig u r e  2 ,   t h er e  ar e   th r ee   m ai n   f u n ct io n s   ar e  B o r r o w   a  b o o k ,   R etu r n   a  b o o k   an d   A d d   a  b o o k .   T h u s ,   th e  ac tiv it y   d iag r a m   o f   L MS   co n s is ts   o f   t h ese  t h r ee   ac tiv itie s .   Fig u r e  6   s h o w s   t h e  ac ti v it y   d iag r a m   o f   A d d   a  b o o k   f u n cti o n   in   L MS.     Fig u r e  3   s h o w s   t h e  ac ti v it y   d i ag r a m   o f   B o r r o w   a   b o o k   f u n c tio n   i n   L M S;  it   d e m o n s tr ate s   w h e n   a n y   u s er   w an ts   to   b o r r o w   a  b o o k   s h o u ld   b e  en ter in g   h is / h er   d etai ls   an d   th e  b o o k   d etails.  L MS  w il l  v er i f y   t h e  u s er   m e m b er s h ip .   I f   it  is   i n co r r ec t,  th e  s y s te m   w ill  d is p la y   a n   er r o r   m es s ag e.   Ot h er w is e,   t h e  s y s te m   w i ll  ch ec k   th e   av ailab ilit y   o f   t h e  b o o k .   I f   it  is   n o t  av ai lab le,   th e  s y s te m   w ill  d is p la y   an   er r o r   m es s ag e.   W h ile,   i f   it  i s   av ailab le,   th e  s y s te m   w ill r ec o r d   th e  b o o k   as len t b o o k ,   d elete   it f r o m   s h el v es a n d   d is p la y   a   s u cc es s   m e s s a g e.           Fig u r e  2 .   T h e  u s e  ca s e  d iag r a m   f o r   L MS       Fig u r e  3 .  A cti v it y   d iag r a m   o f   B o r r o w   a  b o o k   f u n ctio n   in   L M S       Fig u r e  4   s h o w s   t h e  ac ti v it y   d iag r a m   o f   R et u r n   a  b o o k   f u n c t io n   in   L MS ;  it  ex p lai n s   w h e n   an y   u s er   w a n ts   to   r etu r n   a  b o o k   s h o u l d   b e  en ter in g   h is / h er   d etails  an d   th e  b o o k   d etail s .   L MS  w il l  v er i f y   t h e  u s er   m e m b er s h ip .   I f   it  i s   i n co r r ec t,  th e  s y s te m   w ill  d i s p la y   a n   e r r o r   m es s ag e.   Oth er w i s e,   t h e  s y s te m   w ill  v er i f y   f r o m   t h e  b o o k .   I f   it  is   n o t  le n t ,   th e  s y s te m   w ill  d is p la y   a n   er r o r   m es s ag e.   W h i le,   if   it   i s   le n t,  th e  s y s te m   w ill  d elete   it f r o m   b ein g   lo an ,   r ec o r d   it o n   th e  s h el v e s   an d   d is p la y   a  s u cc e s s   m es s ag e.   Fig u r e  5   s h o w s   th e  ac tiv i t y   d i ag r a m   o f   A d d   a  b o o k   f u n ctio n   in   L MS;  i t  s h o w s   w h en   a n y   u s er   w a n t s   to   ad d   a   b o o k   s h o u ld   b e  en ter i n g   h is / h er   d etails   an d   t h e  b o o k   t  d etails.  L M S  w ill  v er i f y   t h e  u s er   m e m b er s h ip .   I f   it  i s   n o t  a  l ib r ar ian ,   th e  s y s t e m   w il l  d is p la y   a n   er r o r   m es s ag e.   E ls e,   t h e  s y s te m   w ill  let  t h e  lib r ar ian   to   e n ter   th e  b o o k   d etails.  T h en ,   ad d   t h e  b o o k   d etails  in to   ca talo g u e  r ec o r d   it  o n   th e  s h el v es  an d   d is p lay   a  s u cc ess   m es s ag e.   E ac h   f u n ctio n   w ith   i ts   r eg ar d in g   ac ti v it y   d iag r a m   w il l  b e  tr an s f o r m   to   Z   s c h e m a ,   w it h   co n s id er atio n   f o r   co n s is ten c y   b et w ee n   UM L   d iag r a m s   a n d   th e  Z   s c h e m a  as   d is cu s s ed   in   t h e  n e x t sectio n .       Evaluation Warning : The document was created with Spire.PDF for Python.
I n t J   E lec  &   C o m p   E n g     I SS N:  2088 - 8708       A n   in teg r a tio n   o f u ml  u s e  ca s e   d ia g r a m  a n d   a ctivity  d ia g r a m  w ith   Z  la n g u a g e…     ( Za in a b   H a s s a n   Mu h a ma d )   3073       Fig u r e  4 .   T h e  ac tiv it y   d iag r a m   o f   R etu r n   a  b o o k   f u n ctio n   in   L M S       Fig u r e   5 .  T h e  ac tiv it y   d iag r a m   o f   A d d   a  b o o k   f u n ctio n   in   L M S       4 . 3 .     Sy s t e m   i m ple m ent a t io n ba s ed  o n f o r m a l sp ec if ica t io ns   T h e  Z   is   a  f o r m al   s p ec i f icati o n   la n g u a g e  f o r   s y s te m   s p ec i f icatio n ,   a n d   it  b a s ed   on   s et   t h eo r y   a n d   m at h e m a tical  lo g ic .   Z   n o tatio n s   e m p lo y ed   i n   i n d u s tr y ;  it   u s ed   in   t h is   p ap er   as  to   b e  th e  m ai n   p ar t  o f   t h e   s o lu tio n   f o r   th is   s t u d y 's  is s u e.   Z   s c h e m as  d escr ib e  th e  s tatic  an d   d y n a m ic  c h ar ac ter is tic s   o f   a  s y s te m   li k e  s tate   tr an s itio n ,   o p er at io n s   an d   r elatio n s h ip s .   T h e  Z   s ch e m as  d es cr ib e  s y s te m   s p ec if ica tio n s   a n d   its   b eh av io u r   to   p r o v id e  s u f f ic ien t   co n f id en ce   b ef o r e  co d in g .   I t  w r itte n   as  t w o   p ar ts ,   t h e  d ec lar atio n   p ar t   d escr ib es  th e  u s ed   v ar iab les  f o r   f u n ct io n ,   an d   th e  o p er atio n   p ar t  d em o n s tr a t es  th e  r elatio n s h ip   b et w ee n   t h e  v al u es  o f   t h o s e   v ar iab les [ 11 ] .   I n   th i s   s ec tio n ,   th e  L MS   s p ec if icatio n s   ar e  i m p le m en ted   b ased   o n   Z   s c h e m a s   an d   u s ed   Z /EV E s   to o l  f o r   v er if icatio n .   Z /EV E s   is   an   in ter ac ti v e  to o l  w h ich   wr ites ,   v er if ie s   an d   an al y s i s   Z   n o tatio n s .   T h is   to o l  p r o v id es  t w o   i n ter f ac e s :  a  g r ap h ical  in ter f ac e  a n d   a  co m m an d   li n e  i n ter f ac e.   B o th   in t er f ac es  s u p p o r t  th e   an al y s is   o f   s p ec if ica tio n s   an d   m an a g e  t h e  s y n c h r o n izati o n   o f   t h e  a n al y s i s   w it h   m o d if icatio n s   to   th e   s p ec if icatio n   [ 8 ] .   T h e  p r o p o s e d   ap p r o ac h   in   t h is   p ap er   in d ic ates  to   in te g r ate  a n d   co n s is tin g   o f   UM L   u s e - ca s e   d iag r a m   an d   ac ti v it y   d iag r a m   w it h   Z   lan g u ag e.   C o n s eq u e n t l y ,   UM L   ac t iv it y   d iag r a m s   co n s tr u cted   b ased   o n   UM L   u s e - ca s e  d ia g r a m   i n   th e  p r ev io u s   s ec tio n .   I n   th is   s e ctio n ,   Z   s p ec i f icatio n   in te r p r eted   f r o m   th e  UM L   ac tiv it y   d iag r a m .   T h e  ac tiv it y   d iag r a m   o f   L MS  co n s is t s   o f   th r ee   ac ti v it y   d ia g r a m s   b ased   o n   th e  m ai n   f u n ctio n s   in   th e   u s e - ca s e   d iag r a m .   E ac h   ac ti v it y   d ia g r a m   h as  t w o   ca s es :  v a lid   ac ti v it y   ca s e  a n d   i n v a lid   ac tiv it y   ca s e.   T h er ef o r e,   Z   s c h e m as   co n s tr u c ted   f o r   t w o   ca s e s   o f   ea ch   ac ti v it y   d iag r a m   as  f o llo w i n g :   Fig u r e  6   s h o w s   Z   Sc h e m a  d ec lar es  th e  p o w er   s ets  B OOK  an d   P E R SON.   I n   ad d itio n ,   w e  r ep r esen t  th e  r esp o n s e  m es s ag e   b y   u s in g   v ar iab le  L MSM E S S A GE .   T h er e  ar e  o n l y   t w o   t y p e s   o f   r esp o n s e ,   w h ic h   ar e   SUC C E SS   o r   F A I L .   L MS   i n it ialized   an d   all  d ef au lt  v alu e s   h av e  b ee n   s e t  t o   in itial  v al u e.   B o o k s   id en tif ied   as   o n _ lo an   an d   o n _ s h el v es.  L ib r ar ian   an d   m e m b er   ar e  th e  s y s te m   u s er s ,   t h e y   d ec lar ed   a s   P E R SON  s et.   I n   ad d itio n   to ,   L en t_ to   is   t h e  r elatio n s h ip   th a t   ca n   e x is t  b et w ee n   a  B o o k   an d   a  P er s o n   as  r ep r esen ted   b y   .           Fig u r e   6 .   Z   Sc h e m a  f o r   I n itiali za tio n   s tate  o f   L M S   Evaluation Warning : The document was created with Spire.PDF for Python.
                      I SS N :   2 0 8 8 - 8708   I n t J   E lec  &   C o m p   E n g ,   Vo l.  9 ,   No .   4 ,  A u g u s t   201 9   :   3 0 6 9   -   3 0 7 6   3074   Fig u r e  7   s h o w s   th e  Z   s c h e m a   is   v er if ied   t h at,   th e  p er s o n   th at  w a n ts   to   b o r r o w   a  b o o k   w a s   r ec o r d ed   as  b ein g   a  lib r ar ian   o r   m e m b e r ,   an d   th e  p ar ticu lar   b o o k   is   av ailab le  ( n o t  alr ea d y   o n   lo an ) .   T h en   th e  b o o k   is   r ec o r d e d   as b ein g   le n t   to   p er s o n   as   r ep r esen ted   b y   ,   an d   t h e  r esp o n s e  ‘ S UC C E SS ’   s h o u ld   b e  o u tp u t.   Fig u r e  8   s h o w s   t h e  Z   s ch e m a  is   v er if ied   th at,   th e  p er s o n   t h at  w an ts   to   b o r r o w   a  b o o k   w as   n o t  r ec o r d ed   as  b ein g   a  lib r ar ian   o r   m e m b er ,   an d   t h e  p ar tic u lar   b o o k   is   n o t  av ai lab le  ( alr ea d y   o n   lo a n ) .   T h en   th e  L M S  s tate  v al u e s   w i ll  n o t   b e  ch an g e  as  r ep r esen ted   b y   an d   th e  r esp o n s e  ‘ F A I L ’   s h o u ld   b e  as  o u tp u t.   Fig u r e  9   s h o w s   t h e  Z   s c h e m a  v er i f ied   t h at,   t h e   p er s o n   t h at  w an ts   to   r etu r n   a   b o o k   r e co r d ed   as  b ein g   a  lib r ar ian   o r   m e m b er ,   an d   t h e  p ar ticu lar   b o o k   r ec o r d ed   as  b ein g   o n   lo an .   T h en   th e   b o o k   i s   r ec o r d ed   as  b ein g   b ac k   o n   th e  s h elv e s ,   th e   r ec o r d   o f   it  b ein g   len t   to   a  p er s o n   is   d elete d   as  r ep r esen ted   b y   an d   th e  r esp o n s e  ‘ S UC C E SS ’   s h o u ld   b e  o u tp u t.   Fig u r e  1 0   s h o w s   t h e  Z   s c h e m a   v er if ied   t h at,   th e  p er s o n   th at   w a n ts   t o   b o r r o w   a  b o o k   w a s   n o t  r ec o r d   as  b ein g   a   lib r ar ian   o r   m e m b er ,   an d   t h e  p ar ticu lar   b o o k   is   n o t  r ec o r d   as  n o t  b ei n g   o n   l o an .   T h en   t h e   L MS   s tate  v al u e s   w ill  n o t  b e  ch an g e   as  r ep r esen ted   b y   an d   th e  r esp o n s e  ‘ F A I L ’   s h o u ld   b e  as  o u tp u t.   F ig u r e  1 1   s h o w s   th e  Z   s c h e m a   v er i f ied   t h at,   t h e  p er s o n   t h at  w a n t s   to   r etu r n   a   b o o k   r ec o r d ed   as  b ein g   a  lib r ar ian .   T h e n   th e  b o o k   s h a ll  b e  ad d   to   t h e  l ib r ar y   ca talo g u e  a n d   t h e  r esp o n s e  ‘ SU C C E SS ’   s h o u ld   b e  a s   o u tp u t.   F ig u r e  1 2   s h o w s   t h e  Z   s c h e m a   v er if ied   t h at,   t h e  p er s o n   t h at   w an ts   t o   b o r r o w   a  b o o k   w a s   n o t  r ec o r d   as  b ein g   a  lib r ar ian .   T h en   th e  L MS  s tate  v al u es  w il l  n o t  b e  ch a n g e   as  r ep r es en ted   b y   an d   th e  r esp o n s e  ‘ F A I L ’   s h o u ld   b e   as   o u tp u t.           Fig u r e  7 .   Z   Sc h e m a  f o r   B o r r o w   a  b o o k   v alid   ca s e  o f   L M S       Fig u r e  8 .   Z   Sc h e m a  f o r   B o r r o w   a  b o o k   in v alid   ca s e  o f   L MS       Fig u r e  9 .   Z   Sc h e m a  f o r   R et u r n   a  b o o k   v alid   ca s e  o f   L M S           Fig u r e.   1 0     Z   Sch e m a  f o r   R et u r n   a  b o o k   in v alid   ca s e  o f   L M S         Fig u r e   11 .   Z   Sch e m a  f o r   A d d   a  b o o k   v alid   ca s e  o f   L M S         Fig u r e   12 .   Z   Sch e m a  f o r   A d d   a  b o o k   in v alid   ca s e  o f   L M S         5.   RE SU L T S AN D  D I SCU SS I O N   T h e  m ai n   co n tr ib u tio n   o f   t h i s   p ap er   is   to   p r o v id e  an   ap p r o ac h   to   co n v er t  f r o m   i n f o r m al  s p ec if icatio n   in to   f o r m al  s p ec if icatio n   b y   f o cu s i n g   o n   i n te g r atio n   an d   co n s i s te n c y   b et w ee n   UM L   s p ec i f icatio n   a n d   f o r m al   m et h o d .   T h e  p r o p o s ed   ap p r o a ch   is   a  f o r m a lizatio n   o f   L ib r ar y   Ma n a g e m en t  S y s te m   ( L MS) .   I t  s tar ts   f r o m   th e   s y s te m 's  r eq u ir e m en t s ,   an d   t h e n   tr an s lated   to   UM L   u s e  ca s e  d iag r a m   a n d   ac tiv it y   d iag r a m .   Fu r th er m o r e  th e  Z   s ch e m as  w er e  ad ap ted   b ased   o n   ac tiv it y   d ia g r a m s .   T h e  s y n ta x   an d   s e m a n tics   o f   L MS   s p ec if icatio n s   ar e  v er if ied   w it h   th e  to o l  Z /EV E S.  I n   th e  p r o p o s ed   ap p r o ac h ,   it  h as  b ee n   s ee n   th at  b r id g ed   a  g ap   b et w ee n   in f o r m al  a n d   f o r m al  m et h o d s .   T h er e  ar e  ce r tain   b en e f its   t o   i m p r o v ed   s y s te m   f ac to r s   d u r in g   a n al y s i s   a n d   d esig n   p h a s es   b ef o r e  i m p le m e n tatio n .   Fo llo w i n g   b en e f it s   ca n   b e  a  r e s u l t o f   t h e  i n te g r atio n   UM L   s p ec i f icatio n  w it h   Z   la n g u a g e:   Evaluation Warning : The document was created with Spire.PDF for Python.
I n t J   E lec  &   C o m p   E n g     I SS N:  2088 - 8708       A n   in teg r a tio n   o f u ml  u s e  ca s e   d ia g r a m  a n d   a ctivity  d ia g r a m  w ith   Z  la n g u a g e…     ( Za in a b   H a s s a n   Mu h a ma d )   3075   5 . 1 .    Reduced  t he  a m big uity     T h is   is   o n e  o f   th e  b i g g est  ad v an ta g e s   th a t  ca n   b e  ac h iev e d   b y   i n te g r atio n   o f   in f o r m a l  an d   f o r m a l   m et h o d s .   T h is   ap p r o ac h   em p h asize s   o n   id en ti f y i n g   t h e  s y s te m   b eh a v io r   b y   u s in g   UM L   b eh av io r   d iag r a m s   ( u s e  ca s e   d iag r a m   an d   ac t iv i t y   d iag r a m )   b ased   o n   s y s te m   r e q u ir e m e n t s .   I n   ad d itio n   to ,   th e  f o r m al   m e th o d s   ar e   m at h e m a ticall y   b ased   tech n iq u es  f o r   s p ec if y in g   a  d escr ip ti o n   o f   th e  s y s te m   to   b e  d ev elo p ed .   T h er ef o r e,   th e  s y s te m   r eq u ir e m e n ts   s p ec if ica tio n   w ill b e  clea r l y   d ef in ed     5 . 2 .    Reduced  t he  e rr o r     T h is   is   o n e  o f   th e  m o s t  i m p o r tan t  asp ec ts   o f   t h e  s o f t war e  d esig n .   T h e  p r o p o s ed   ap p r o ac h   is   ce r tify in g   a  d e v elo p ed   s y s te m ,   b y   g e n er ati n g   m o d els   b ased   o n   s y s te m 's   r eq u ir e m en ts   b y   u s i n g   t h e  R a tio n al   R o s e  to o l  to   cr ea te  a  co m p let e  UM L   d ia g r a m s .   A n d   t h en   u s e s   f o r m a l  m e th o d s   to   g e n er ate  p r o o f s   th at  t h e   s ch e m a  m ee ts   r eq u ir e m en t s .   Mo r eo v er   th e  s c h e m as  ar e  v er if ied   b y   u s in g   Z /EV E S  c h ec k er   to o l,  to   o v er co m e   th e  er r o r s .     5 . 3 .    I m pro v ed  t he  q ua lity   Fo r m al  m eth o d s   u s e  m at h e m a tical  an d   lo g ical  f o r m aliza tio n .   Fo r m al  m eth o d s   h a v e  b ee n   u s ed   in   o u r   ap p r o ac h ,   s tar tin g   f r o m   t h e  d esig n   p h ase  to   f i n d   d ef ec t s .   T h e  b asic  p u r p o s e  is   to   i m p r o v e  th e  q u alit y   o f   t h e   r esu lti n g   s o f t w ar e.   T h er ef o r e,   f o r m al  m et h o d s   w er e  t h e  b est   w a y   to   i m p r o v e  s o f t w ar e  q u alit y   ca n   b e  ap p lied   in   ea r l y   s tag e s   o f   t h e  So f t w a r e  Dev elo p m e n t  L if e  C y cle  ( SD L C ) .     5 . 4 .    Co nfident ia lity   W e  an ticip ate  th at   s o f t w ar e  s e cu r it y   ca n   b e  i m p r o v ed   t h r o u g h   t h e  ap p licatio n   o f   f o r m al   m e th o d s .   B y   i m p le m en t in g   Z   s c h e m a   f o r   ea ch   f u n ctio n   o f   t h at  s o f t w ar e.   T h u s ,   it   m a k es   it   ea s ier   to   m a n ag e   an d   i m p le m e n t   th e  co d e  an d   m ak e  it  s ec u r e  ag ain s t  u n a u t h o r ized   ac ce s s .   W ith   th i s   w e  ca n   s o r t  th a t  w h ich   u s er   ca n   ac ce s s   w h at  t y p e  o f   in f o r m at io n .   So   t h e  in f o r m at io n   is   p r o tecte d .   B r ief l y ,   th e  r es u lts   o f   t h e  in te g r atio n   UM L   s p ec if ica tio n   w i th   f o r m al  s p ec i f icatio n   ar e  r e d u ce d   th e   a m b ig u it y   a n d   E r r o r ,   an d   I m p r o v ed   th e  q u ali t y   a n d   co n f id en t ialit y   o f   t h e  s y s te m   i n   t h e  ea r l y   s ta g es.  H o w e v er ,  t h e  li m itatio n   o f   t h e  p r o p o s e d   ap p r o ac h   is   th a t  it  d o es  n o t  s u p p o r t  co d e  g en er atio n .   E v en   i f   t h e  p r o p o s ed   ap p r o ac h   to   d esig n   L M S  d o es  n o t  p r o v id e  th e  f in e - g r ain e d   s tep s   an d   p r ac tices  f o r   i m p letatio n   p h a s e,   th e   d ev elo p m en t   p r o ce s s es   in   t h is   p ap er   allo w   th e   s o f t w ar e  d e v elo p er   to   d escr ib e  an d   ca p t u r e  th e   a n al y s i s   a n d   d esig n   p h a s es  f o r   L MS.   Ho wev er ,   s i n ce   t h e  s tan d ar d   Z   n o tatio n s   u s ed   to   s u p p o r t  th e  co d e  g e n er atio n   b y   a n y   p r o g r am m i n g   lan g u ag e.       6.   CO NCLU SI O N   T h is   p ap er   p r o p o s ed   an   ap p r o ac h   to   f o r m aliza tio n   o f   L i b r ar y   Ma n a g e m e n t   S y s te m   ( L MS)   b y   f o cu s in g   o n   i n te g r atio n   a n d   c o n s is ten c y   b et w ee n   U ML   s p e cif icatio n   a n d   f o r m al  m et h o d .   T h e  b eh av io r   o f   th e   s y s te m   i s   s p ec i f ied   f r o m   s y s t e m ' s   r eq u ir e m e n t s ,   a n d   t h en   t r an s lated   to   UM L   u s e   ca s e   d iag r a m   an d   ac tiv it y   d iag r a m .   Mo r eo v er   t h e  Z   s ch e m as  w er e  ad ap ted   b ased   o n   ac tiv i t y   d ia g r a m s .   T h e  s y n ta x   an d   s e m a n tics   o f   L MS   s p ec i f icatio n s   ar e  v er if i ed   w it h   t h e  Z /EV E S  to o l.  T h e  p r o p o s ed   ap p r o ac h   is   an   i n teg r atio n   o f   UM L   s p ec if icatio n   w it h   Z   la n g u a g e,   as  a  r esu l t  th a t  h a s   b ee n   b r id g ed   a  g ap   b et w ee n   in f o r m al  a n d   f o r m al   m et h o d s .   T h e  o b tain ed   r esu l ts   w er e  to   i m p r o v e   t h e  s y s te m 's   r eq u ir e m en ts   d u r i n g   an al y s is   an d   d es i g n   p h a s es  in   ter m s   r ed u ce d   th e  a m b i g u i t y   a n d   er r o r ,   im p r o v ed   th e  q u al it y   a n d   co n f id e n tialit y .       ACK NO WL E D G E M E NT S     T h e  au th o r s   w o u ld   li k e  to   th a n k   th e  U n i v er s it y   o f   K u f a,   Min i s tr y   o f   Hi g h er   E d u ca tio n   a n d   Scien ti f ic  R esear ch   ( Mo HE S R ) ,   Dir ec to r ate  o f   E d u ca tio n   i n   Naj af   an d   th e  I r aq i M in is tr y   o f   E d u ca tio n   f o r   th eir   s u p p o r t  w it h   co llab o r atio n   an d   as s is ta n ce   in   t h i s   r esear ch .       RE F E R E NC E S       [ 1 ]   N.  Ib ra h im ,   R.   Ib ra h im ,   M .   Z.   S a rin g a t ,   D.  M a n so r  &   T .   He r a w a n ,   " Co n siste n c y   ru les   b e t w e e n   UM L   u se   c a se   a n d   a c ti v it y   d iag ra m s      u sin g   l o g ica l  a p p r o a c h ,"   In ter n a ti o n a l  J o u rn a l  o f  S o ft wa re   E n g i n e e rin g   a n d   it s  Ap p l ica ti o n s ,  V o l .   5 ,   No .   3 ,   p p .   1 1 9 - 1 3 4 ,   2 0 1 1 .   [ 2 ]   B.   M o n d a l ,   B.   Da s  &   P .   Ba n e rje e ,   " F o rm a l  S p e c if ic a ti o n   o f   UML   Us e   Ca se   Dia g ra m - A   C A S L   Ba se d   A p p ro a c h , "   In ter n a t io n a l  J o u rn a l  o f  C o mp u ter   S c ien c e   a n d   I n fo rm a ti o n   T e c h n o lo g ies ,   V o l .   5 ,   No .   9 ,   p p . 2 1 1 3 - 2 7 1 7 ,   2 0 1 4 .   [ 3 ]   B.   F a lah ,   M .   A k o u r,   I.   A ra b   &   Y.  M ’h a n n a ,   " A n   A tt e m p t  T o w a rd s  a   F o rm a li z in g   U M L   Clas s  Dia g ra m   S e m a n ti c s , "   In   Pro c e e d in g s  o f  th e   Ne w  T re n d s  in   In f o rm a ti o n   T e c h n o l o g y   ( NT IT - 2 0 1 7 ),   T h e   Un ive rs it y   o f  J o rd a n ,   Amma n ,   J o rd a n ,   p p .   2 1 - 27 ,  25 - 27 ,   A p ril   2 0 1 7 .   Evaluation Warning : The document was created with Spire.PDF for Python.
                      I SS N :   2 0 8 8 - 8708   I n t J   E lec  &   C o m p   E n g ,   Vo l.  9 ,   No .   4 ,  A u g u s t   201 9   :   3 0 6 9   -   3 0 7 6   3076   [ 4 ]   N.  M .   M in h a s,  A .   M .   Qa z i,   S .   S h a h z a d i  &   S .   G h a f o o r,   " A n   In te g ra ti o n   o f   UML   S e q u e n c e   Dia g ra m   w i th   F o rm a l   S p e c if ica ti o n   M e th o d s - A   F o rm a l  S o lu ti o n   Ba se d   o n   Z , "  J o u rn a l  o f   S o ft w a re   En g i n e e rin g   a n d   Ap p li c a ti o n s ,   Vo l.   8 ,   No .   8 ,   p p .   3 7 2 - 3 8 3 ,   2 0 1 5 .   [ 5 ]   M .   S i n g h ,   A .   K.  S h a rm a   &   R.   S a x e n a ,   " W h y   F o rm a l  M e th o d s   A re   Co n sid e re d   f o r  S a f e t y   Crit ica l  S y st e m s? ,"   J o u rn a l  o f  S o ft w a re   En g in e e rin g   a n d   Ap p li c a ti o n s ,   V o l.   8 ,   No .   1 0 ,   p p .   5 3 1 - 538 ,   2 0 1 5 .   [ 6 ]   M .   S i n g h ,   A .   K.  S h a rm a   &   R.   S a x e n a ,   " F o rm a l  T ra n s f o r m a ti o n   o f   UML   Dia g ra m :  Us e   Ca se ,   Clas s,  S e q u e n c e   Dia g ra m   w it h   Z  No tatio n   f o r  R e p re se n ti n g   th e   S tati c   a n d   Dy n a m ic  P e rsp e c ti v e s  o f   S y ste m , "   In   Pro c e e d in g s  o f   In ter n a t io n a l  C o n fer e n c e   o n   ICT   fo r S u sta i n a b le De v e lo p me n t ,   S p r in g e r S in g a p o re ,   p p .   2 5 - 3 8 ,   2 0 1 6 .   [ 7 ]   S .   H.  Ba k ri,   H.  Ha ru n ,   A .   A l z o u b i,   R.   Ib ra h im ,   Z.   Ja m a lu d in ,   N.  Ch e P a   &   M .   S .   A .   Ba k a r,   " T h e   f o r m a l  sp e c if ic a ti o n   f o r  th e   in v e n to ry   s y ste m   u sin g   Z  lan g u a g e ,"   In   Pro c e e d in g s  4 th   In ter n a ti o n a l  Co n fer e n c e   o n   Co mp u t in g   a n d   In f o rm a ti c s(   ICOCI) ,   p p .   2 8 - 30 ,   2 0 1 3 .   [ 8 ]   P .   S a ra th a ,   G .   V .   U m a   &   B.   S a n th o sh ,   " F o rm a l  S p e c if i c a ti o n   f o r  On li n e   F o o d   Ord e rin g   S y ste m   Us in g   Z   L a n g u a g e , "  In   Pro c e e d in g s  o f  I n ter n a ti o n a l  C o n fer e n c e   o n   Rec e n t  T re n d s  a n d   C h a ll e n g e s  i n   Co mp u t a ti o n a l   M o d e ls ( ICRT CCM ),   S e c o n d   In te rn a ti o n a l,   IE EE ,    p p .   3 4 3 - 3 4 8 ,   2 0 1 7 .   [ 9 ]   P .   S ric h e tt a ,   " Co n c e p t u a l  F ra m e w o rk   o f   T ra n s f o rm in g   In f o r m a l  Re q u irem e n ts  S p e c if ica ti o n   to   Z  S p e c if ica ti o n ,"   In   Pro c e e d in g s  o f  I n ter n a ti o n a l   Co n fer e n c e   o n   C o mp u ter   a n d   S o ft w a re   M o d e li n g   IPC S IT ,   S i n g a p o r e ,    p p .   1 9 - 2 4 ,   2 0 1 1 .   [ 10 ]   M .   Ba tra,  " F o r m a l  m e th o d s:  Be n e f it s,  c h a ll e n g e s  a n d   f u tu re   d irec ti o n , "   J o u rn a l  o f  Gl o b a l  Res e a rc h   in   Co mp u ter   S c ien c e ,   Vo l.   4 ,   N o .   5 ,   p p .   2 1 - 25 ,   2 0 1 3 .   [ 11 ]   M .   W .   A z e e m ,   M .   A h sa n ,   N.  M .   M in h a s  &   K.  No re e n ,   " S p e c i f ica t io n   o f   e - He a lt h   s y ste m   u sin g   Z:   A  m o ti v a ti o n   to   f o r m a l  m e th o d s , "   In   Pro c e e d in g s  In ter n a ti o n a l  Co n fer e n c e   fo r  Co n v e rg e n c e   o f  T e c h n o l o g y   ( ICCT ),   IEE E ,    p p .   1 - 6 ,   2 0 1 4 .   [ 12 ]   S .   A .   Kh a n   &   H.  Ja m sh e d ,   " A n a ly sis  o f   f o r m a l  m e th o d s  f o r  sp e c if ica ti o n   o f   e - Co m m e rc e   a p p li c a ti o n s , "   M e h ra n   Un ive rs it y   Res e a rc h   J o u rn a l  Of  E n g i n e e rin g   &   T e c h n o lo g y ,   V o l.   3 5 ,   No .   1 ,   p p .   1 9 - 28 ,   2 0 1 6 .   [1 3 ]   D .   K .   Kim ,   " D e v e lo p m e n t  o f   M o b il e   Cl o u d   A p p li c a ti o n s  u si n g   UML , "   In ter n a ti o n a l  J o u rn a l  o f   El e c trica l  a n d   Co mp u ter   E n g in e e rin g   ( IJ ECE ),   V o l .   8 ,   No .   1 ,   p p .   5 9 6 - 6 0 4 ,   F e b r u a r y   2 0 1 8 .   [1 4 ]   A .   L a sb a h a n i,   M .   Ch h ib a   &   A .   T a b y a o u i ,   " A   UM L   P ro f il e   f o r  S e c u rit y   a n d   Co d e   G e n e ra ti o n , "   In ter n a ti o n a l   J o u rn a l  o f  El e c trica l  a n d   C o mp u t e r E n g i n e e rin g   ( IJ ECE ),   V o l . 8 ,   No . 6 ,   p p .   5 2 7 8 - 5 2 9 1 ,   De c e m b e r   2 0 1 8 .       B I O G RAP H I E S   O F   AUTH O RS        Za in a b   H a ss a n   M u h a m a d   r e c e iv e d   th e   Ba c h e lo r’s  d e g re e   in   Co m p u ter  S c in e c e   f ro m   Un iv e rsit y   o f   Ba b y lo n ,   Ira q ,   in   2 0 0 7 ,   a n d   th e   M a ste r’s  d e g re e   in   S o f twa re   En g in e e rin g   f ro m   Un iv e rsiti   T u n   Hu ss e in   On n   M a la y sia   (U T HM),   Ba tu   P a h a t,   M a la y sia .   S h e   is  c u rre n tl y   a   L e c tu re r  o f   Co m p u ter  S c ien c e   a t   Dire c to ra te  o f   Ed u c a ti o n ,   Ira q i  M in istry   o f   Ed u c a ti o n ,   Na jaf ,   Ira q   . He r  re se a rc h   in tere sts in c lu d e   so f t w a re   e n g in e rin g ,   so f t w a r e   te stin g   a n d   f o rm a l  m e th o d .           Dh a f e r   A b d u la m e e r   Abd u l m o n i m   re c e i v e d   th e   Ba c h e lo r’s  d e g re e   in   Co m p u ter  S c in e c e   f ro m   Un iv e rsit y   o f   Ba b y lo n ,   Ba b il ,   Ir a q ,   in   2 0 0 7 ,   a n d   t h e   M a ste r’s  d e g re e   in   S o f twa re   En g in e e rin g   f ro m   Un iv e r siti   T u n   Hu ss e in   O n n   M a lay sia   (U T HM),   Ba tu   P a h a t,   M a lay sia ,   in   2 0 1 5 .   He   is  c u rre n tl y   a   Lec tu re r  o f  Co m p u ter  S c ien c e   a t  Dire c to ra te  o f  Ed u c a ti o n ,   a n d   Op e n   E d u c a ti n a l   Co ll e g e ,   Na ja f ,   Ira q .   His  re se a r c h   in tere sts  in c lu d e   so f tw a re   e n g in e rin g ,   so f tw a r e   tes ti n g   a n d   f o r m a l  m e th o d .           B a sh a r   Ala t h a r i   re c e iv e d   a   M . S c .   d e g re e   in   so f tw a re   e n g in e e rin g   f ro m   Un iv e rsit y   o f   UT HM  in   2 0 1 5   f ro m   M a la y sia .   He   is  w o rk in g   lec tu re   a n d   Re se a rc h e r  in   u n iv e rsity   o f   k u f a ,   I T RDC.   Am o n g   h is r e se a rc h   in tere sts a re   r e se a rc h   in   so f twa re   e n g in e e rin g   a n d   n e tw o rk in g .       Evaluation Warning : The document was created with Spire.PDF for Python.