I nte rna t io na l J o urna l o f   E lect rica l a nd   Co m p ute 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 u m l  use cas dia g ra m   a nd   a ctivity   dia g ra m   w ith  Z   la ng ua g e f o for m a li z a t io o 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 A bd ul m o n i m 2 B a s ha 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 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 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 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 h a n d ,   f o rm a m e th o d s a re   tec h n iq u e a n d   to o ls  u se   th e   m a th e m a ti c a 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 o f   th e   u n a m b ig u o u 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 S o f t w a re   De v e lo p m e n 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 so f t wa re   s y ste m s.  T h is  p a p e p ro p o se a n   a p p r o a c h   i n v o lv e 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 w it h   lan g u a g e   f o 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 S y ste m   (L M S ).   T h e   f o c u o f   th is   p a p e 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   S c h e m a ,   a n d   th e n   v e rif ied   b y   u sin g   t h e   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 ©   2 0 1 9   In stit u te o 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 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 ( UM L )   i s   v i s u al  la n g u a g 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   g r ap h i ca n o tatio n   w i th   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 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  s ta n d ar d   to o to   co m p o s 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 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 is   th lack   o f   p r ec is io n   in   t h 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 d if f er e n in ter p r etati o n   o f   th d escr ib ed   m o d el.   I n   ad d itio n   to ,   t h 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,   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 n g i n ee r in g ,   th 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 v er y   u s ef u to   u n d er s ta n d   th 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 tech n iq u es  b ased   o n   m at h e m atica n o t atio n s ,   w h ich   p la y   cr itical  r o le  as  th e y   f o c u s   o n   r ef in e m e n o f   r eq u ir e m e n ts   i n   th i n itia s ta g es  o f   t h S y s te m   De v elo p m e n L i f C y cl ( SDLC)  lik 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 u s ed   to   en s u r 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 p r ec is el y   ex p r ess .   I n   o r d er   to   r ef in e m e n o f   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 in cr ea s 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 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 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 p h a s es  [ 8 ,   9 ] .   T h 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 d esi g n   ti m e,   it  also   ad d r ess es  i m p r o v 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 w id el y   u s ed   f o r   d ev elo p m e n 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 ar v a r io u s   f o r m al  la n g u a g e s   li k VDM ,   B - Me t h o d s ,   L ar ch   a n d   Z   n o tatio n   ar u s ed   f o r   f o r m a s p ec if ica tio n .   Z   n o tatio n   is   g o o d   ex a m p l b ased   o n   f o r m a l   s p ec if icatio n   lan g u ag w h ich   u s es  t h s et  th eo r y   f o r   d eter m i n in g   t h b eh av io r   o f   s eq u e n tial  s y s te m s   [ 1 1 ] .   T h liter atu r i n d icate s   t h at  th m o s t   w ell - k n o w n   is s u 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 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 q u ali t y .   i n   ad d itio n ,   t h m o s 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 u s 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 f o r m al  s p ec if ic atio n s   h av n o b ee n   m ad f r o m   ac ti v it y   d iag r a m .   Hen ce ,   t h 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 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 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 a m o n g   UM L   us ca s 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 w a s   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 Z /EV E S to o l.     T h 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 r elate d   w o r k .   Secti o n   3   f u ll y   d escr ib es  th 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 ca s 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 r es u lt s   o f   t h c ase  s t u d y   to   d e m o n s tr ate  th 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 s tr en g t h   an d   w ea k n ess   o f   th 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 co n clu s i o n s .       2.   RE L AT E WO RK S   T h 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 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 o f f er ed   it  in   d if f er en a s p ec ts .   T h 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 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 f o r   d ev elo p ed .   T h Fli g h 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 m o r th a n   o n U ML   d iag r a m ,   i n   o r d er   to   th r es u lts   ca n   b m o r 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 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 R o ad   T r af f ic  Ma n ag e m e n 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 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 u s ed .   Mo r eo v er ,   th Z /E VE s   to o u s ed   to   v er if y   Z   s c h e m a s .   I n   th r esear ch   p r o v id ed   f r o m   B ak r et  al.   [ 7 ] ,   r elate d   to   o u r   r esear ch   s tu d y   w h er 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 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 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 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 f o r   d ev elo p in g   t h 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 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 ca s d iag r a m   a n d   Z   s c h e m as  t o   i m p r o v s o f t w ar 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 an d   co s t   at  an   i n itia s ta g e.   Ho w e v er ,   in   [ 8 ]   h av b ee n   u s ed   Z /EV E s   to o 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 co m p ar ativ 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 th 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 ca s e   d ia g r a a n d   a ctivity  d ia g r a w ith   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 liter atu r in d icate s   th a th m o s 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 ca s e,   class ,   s eq u e n ce .   T h f o r m al  s p ec i f icatio n s   d id   n o 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 ca s 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 to   d esig n   t h L M S.  I n   ad d itio n   to ,   w h av d is c u s s ed   ea r lier   th at  th m o s well - k n o w n   is s u f o r   UM L   is   lack   o f   clea r   s e m an t ics,  d if f er en i n ter p r etatio n   o f   th 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 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 A ND  AN AL Y SI S     UM L   i s   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 co n s i s ten c y   is   s ig n i f ica n r u le  b et w ee n   d iag r a m s ,   to   en s u r th at  i m p le m en tatio n   o f   th d ia g r a m s   is   co m p le m en t in g .   Mo r eo v er ,   th co n s is te n c y   b et w ee n   u s e - ca s 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 o t h er   h an d ,   Fo r m al  m e th o d s   ar 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 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 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 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 ca s d iag r a m   an d   ac ti v it y   d iag r a m )   w it h   t h f o r m al   s p ec if icatio n   la n g u a g ( 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 t y p ch ec k er   to o l.  T h is   to o u s ed   f o r   v er if y i n g   th s c h e m s p ec if ica tio n ,   th a w r o te  b ased   o n   Z   n o tatio n   la n g u a g [ 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 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 f o r m a m et h o d   as s h o w n   i n   Fig u r 1 .           Fig u r 1 .   T h 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 AND  AP P R O ACH   M O DE L L I N G   I n   th is   p ap er ,   w p r esen ca s s tu d y   o f   A   L ib r ar y   Ma n ag e m en 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   u s er   w a n ts   to   b o r r o w   b o o k ,   t h s y s te m   s h o u ld   b ab le  to   v er if y   th m e m b er s h ip   o th u s er   f ir s t,  if   t h u s er   is   a   m e m b er ,   th e n   t h s y s te m   c h ec k s   t h av ai lab ilit y   o f   t h b o o k .   I f   th b o o k   is   av ailab le,   th e n   th s y s te m   lets   th m e m b er   r eser v es  t h b o o k   an d   th d atab ase  n ee d s   to   u p d ate  to   in d icate   th at   th b o o k   is   n o av a ilab le  an y m o r e.   T h f ir s s tep   is   to   d eter m i n t h r eq u ir e m e n t s   an al y s i s   f o r   t h s ce n ar io   as   in   th 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 an al y s is   s tag w as  t h b asis   o f   th 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 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 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 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 n ee d   to   v er if y   th m e m b er s h ip   o f   t h 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 n ee d   to   v er i f y   th m e m b er s h ip   o f   t h u s er   an d   th e   leg a lit y   o f   t h b o o k .   L ib r ar ian   tas k   w as   to   m ain t ain   t h n e w   b o o k   in f o r m atio n   ad d itio n .   T h s t ak eh o ld er s   o f   th s y s te m   ar e   L ib r ar ian   a n d   Me m b er .   T h s y s te m   h a s   b asic   f u n ctio n s   t h at  ar Ver if y   m e m b er s h ip ,   C h ec k   b o o k   a v ailab ilit y ,   B o r r o w   b o o k ,   R etu r n   b o o k   a n d     A d d   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 ab o v an al y s i s ,   w t h en   d r a w   t h d iag r a m s   o f   UM L   m ain l y   t h u s ca s 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 R atio n al  R o s 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 2   s h o w s   u s ca s d iag r a m   f o r   t h L M S.  T h er ar t w o   u s er s   to   u s t h s y s te m ,   w h i ch   ar 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   b o o k ,   R etu r n   b o o k   a n d   A d d   b o o k .   A s   Me m b er   ca n   d o   ac tiv ities   f o r   B o r r o w   b o o k   an d   R et u r n   a   b o o k .   W h ile ,   th 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   b o o k ' s   av ailab il it y   ar 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 u s ca s d ia g r a m   in   Fig u r 2 ,   t h er ar e   th r ee   m ai n   f u n ct io n s   ar B o r r o w   b o o k ,   R etu r n   b o o k   an d   A d d   b o o k .   T h u s ,   th 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 6   s h o w s   t h ac ti v it y   d iag r a m   o f   A d d   b o o k   f u n cti o n   in   L MS.     Fig u r 3   s h o w s   t h 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   b o o k   s h o u ld   b en ter in g   h is / h er   d etai ls   an d   th b o o k   d etails.  L MS  w il v er i f y   t h u s er   m e m b er s h ip .   I f   it  is   i n co r r ec t,  th 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 s y s te m   w i ll  ch ec k   th e   av ailab ilit y   o f   t h b o o k .   I f   it  is   n o av ai lab le,   th 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 s y s te m   w ill r ec o r d   th 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 2 .   T h u s ca s d iag r a m   f o r   L MS       Fig u r 3 A cti v it y   d iag r a m   o f   B o r r o w   b o o k   f u n ctio n   in   L M S       Fig u r 4   s h o w s   t h ac ti v it y   d iag r a m   o f   R et u r n   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   b o o k   s h o u l d   b en ter in g   h is / h er   d etails  an d   th b o o k   d etail s .   L MS  w il v er i f y   t h u s er   m e m b er s h ip .   I f   it  i s   i n co r r ec t,  th 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 s y s te m   w ill  v er i f y   f r o m   t h b o o k .   I f   it  is   n o le n t ,   th 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 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 s h el v e s   an d   d is p la y   s u cc e s s   m es s ag e.   Fig u r 5   s h o w s   th ac tiv i t y   d i ag r a m   o f   A d d   b o o k   f u n ctio n   in   L MS;  i 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 en ter i n g   h is / h er   d etails   an d   t h b o o k   d etails.  L M w ill  v er i f y   t h u s er   m e m b er s h ip .   I f   it  i s   n o l ib r ar ian ,   th s y s t e m   w il d is p la y   a n   er r o r   m es s ag e.   E ls e,   t h s y s te m   w ill  let  t h lib r ar ian   to   e n ter   th b o o k   d etails.  T h en ,   ad d   t h b o o k   d etails  in to   ca talo g u r ec o r d   it  o n   th s h el v es  an d   d is p lay   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 b 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 Z   s c h e m as   d is cu s s ed   in   t h 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 ca s e   d ia g r a a n d   a ctivity  d ia g r a w ith   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 4 .   T h ac tiv it y   d iag r a m   o f   R etu r n   b o o k   f u n ctio n   in   L M S       Fig u r e   5 T h ac tiv it y   d iag r a m   o f   A d d   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 Z   is   f o r m al   s p ec i f icati o n   la n g u a g 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 th m ai n   p ar 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 th s tatic  an d   d y n a m ic  c h ar ac ter is tic s   o f   s y s te m   li k 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 Z   s ch e m as  d es cr ib 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 s u f f ic ien t   co n f id en ce   b ef o r co d in g .   I w r itte n   as  t w o   p ar ts ,   t h d ec lar atio n   p ar t   d escr ib es  th u s ed   v ar iab les  f o r   f u n ct io n ,   an d   th o p er atio n   p ar d em o n s tr a t es  th r elatio n s h ip   b et w ee n   t h 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 L MS   s p ec if icatio n s   ar 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 f o r   v er if icatio n .   Z /EV E s   is   an   in ter ac ti v to o 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 p r o v id es  t w o   i n ter f ac e s g r ap h ical  in ter f ac a n d   co m m an d   li n i n ter f ac e.   B o th   in t er f ac es  s u p p o r th e   an al y s is   o f   s p ec if ica tio n s   an d   m an a g t h s y n c h r o n izati o n   o f   t h 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 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 d ia g r a m   i n   th 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 UM L   ac tiv it y   d iag r a m .   T h 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 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 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 6   s h o w s   Z   Sc h e m d ec lar es  th p o w er   s ets  B OOK  an d   P E R SON.   I n   ad d itio n ,   w r ep r esen th r esp o n s 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 ar 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 b ee n   s e 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 th 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 r elatio n s h ip   th a t   ca n   e x is b et w ee n   B o o k   an d   P er s o n   as  r ep r esen ted   b y   .           Fig u r e   6 .   Z   Sc h e m 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 7   s h o w s   th Z   s c h e m a   is   v er if ied   t h at,   th p er s o n   th at  w a n ts   to   b o r r o w   b o o k   w a s   r ec o r d ed   as  b ein g   lib r ar ian   o r   m e m b e r ,   an d   th p ar ticu lar   b o o k   is   av ailab le  ( n o alr ea d y   o n   lo an ) .   T h en   th 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 r esp o n s S UC C E SS   s h o u ld   b o u tp u t.   Fig u r 8   s h o w s   t h Z   s ch e m is   v er if ied   th at,   th p er s o n   t h at  w an ts   to   b o r r o w   b o o k   w as   n o r ec o r d ed   as  b ein g   lib r ar ian   o r   m e m b er ,   an d   t h p ar tic u lar   b o o k   is   n o av ai lab le  ( alr ea d y   o n   lo a n ) .   T h en   th L M s tate  v al u e s   w i ll  n o t   b ch an g as  r ep r esen ted   b y   an d   th r esp o n s F A I L   s h o u ld   b as  o u tp u t.   Fig u r 9   s h o w s   t h Z   s c h e m 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   lib r ar ian   o r   m e m b er ,   an d   t h 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 s h elv e s ,   th e   r ec o r d   o f   it  b ein g   len t   to   p er s o n   is   d elete d   as  r ep r esen ted   b y   an d   th r esp o n s S UC C E SS   s h o u ld   b o u tp u t.   Fig u r 1 0   s h o w s   t h Z   s c h e m a   v er if ied   t h at,   th p er s o n   th at   w a n ts   t o   b o r r o w   b o o k   w a s   n o 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 p ar ticu lar   b o o k   is   n o r ec o r d   as  n o 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 b ch an g e   as  r ep r esen ted   b y   an d   th r esp o n s F A I L   s h o u ld   b as  o u tp u t.   F ig u r 1 1   s h o w s   th Z   s c h e m a   v er i f ied   t h at,   t h 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   lib r ar ian .   T h e n   th b o o k   s h a ll  b ad d   to   t h l ib r ar y   ca talo g u a n d   t h r esp o n s SU C C E SS   s h o u ld   b a s   o u tp u t.   F ig u r 1 2   s h o w s   t h Z   s c h e m a   v er if ied   t h at,   t h p er s o n   t h at   w an ts   t o   b o r r o w   b o o k   w a s   n o r ec o r d   as  b ein g   lib r ar ian .   T h en   th L MS  s tate  v al u es  w il n o b ch a n g e   as  r ep r es en ted   b y   an d   th r esp o n s F A I L   s h o u ld   b e   as   o u tp u t.           Fig u r 7 .   Z   Sc h e m f o r   B o r r o w   b o o k   v alid   ca s o f   L M S       Fig u r 8 .   Z   Sc h e m f o r   B o r r o w   b o o k   in v alid   ca s o f   L MS       Fig u r 9 .   Z   Sc h e m f o r   R et u r n   b o o k   v alid   ca s o f   L M S           Fig u r e.   1 0     Z   Sch e m f o r   R et u r n   b o o k   in v alid   ca s o f   L M S         Fig u r e   11 .   Z   Sch e m f o r   A d d   b o o k   v alid   ca s o f   L M S         Fig u r e   12 .   Z   Sch e m f o r   A d d   b o o k   in v alid   ca s o f   L M S         5.   RE SU L T S AN D I SCU SS I O N   T h 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 an   ap p r o ac h   to   co n v er 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 p r o p o s ed   ap p r o a ch   is   f o r m a lizatio n   o f   L ib r ar y   Ma n a g e m en S y s te m   ( L MS) .   I 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 ca s d iag r a m   a n d   ac tiv it y   d iag r a m .   Fu r th er m o r th Z   s ch e m as  w er ad ap ted   b ased   o n   ac tiv it y   d ia g r a m s .   T h 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 v er if ied   w it h   th to o Z /EV E S.  I n   th 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   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 ar 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 i m p le m e n tatio n .   Fo llo w i n g   b en e f it s   ca n   b r e s u l t o f   t h i n te g r atio n   UM L   s p ec i f icatio 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 ca s e   d ia g r a a n d   a ctivity  d ia g r a w ith   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 o f   th b i g g est  ad v an ta g e s   th a ca n   b ac h iev e d   b y   i n te g r atio n   o f   in f o r m a 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 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 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 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   d escr ip ti o n   o f   th s y s te m   to   b d ev elo p ed .   T h er ef o r e,   th s y s te m   r eq u ir e m e n ts   s p ec if ica tio n   w ill b clea r l y   d ef in ed     5 . 2 .    Reduced  t he  e rr o r     T h is   is   o n o f   th m o s i m p o r tan asp ec ts   o f   t h s o f t war d esig n .   T h p r o p o s ed   ap p r o ac h   is   ce r tify in g   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 R a tio n al   R o s to o to   cr ea te  co m p let UM L   d ia g r a m s .   A n d   t h en   u s e s   f o r m a 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 m ee ts   r eq u ir e m en t s .   Mo r eo v er   th s c h e m as  ar v er if ied   b y   u s in g   Z /EV E c h ec k er   to o l,  to   o v er co m e   th 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 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 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 d esig n   p h ase  to   f i n d   d ef ec t s .   T h b asic  p u r p o s is   to   i m p r o v th 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 t h b est   w a y   to   i m p r o v s o f t w ar q u alit y   ca n   b ap p lied   in   ea r l y   s tag e s   o f   t h So f t w a r Dev elo p m e n L if C y cle  ( SD L C ) .     5 . 4 .    Co nfident ia lity   W an ticip ate  th at   s o f t w ar s e cu r it y   ca n   b i m p r o v ed   t h r o u g h   t h 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 co d an d   m ak it  s ec u r ag ain s u n a u t h o r ized   ac ce s s .   W ith   th i s   w ca n   s o r th a w h ich   u s er   ca n   ac ce s s   w h at  t y p o f   in f o r m at io n .   So   t h in f o r m at io n   is   p r o tecte d .   B r ief l y ,   th r es u lts   o f   t h 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 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 q u ali t y   a n d   co n f id en t ialit y   o f   t h s y s te m   i n   t h ea r l y   s ta g es.  H o w e v er t h li m itatio n   o f   t h p r o p o s e d   ap p r o ac h   is   th a it  d o es  n o s u p p o r co d g en er atio n .   E v en   i f   t h p r o p o s ed   ap p r o ac h   to   d esig n   L M d o es  n o p r o v id th 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 d e v elo p er   to   d escr ib an d   ca p t u r 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 s tan d ar d   Z   n o tatio n s   u s ed   to   s u p p o r th co d 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 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 Z   s ch e m as  w er ad ap ted   b ased   o n   ac tiv i t y   d ia g r a m s .   T h 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 v er if i ed   w it h   t h Z /EV E to o l.  T h 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  r esu l th a h a s   b ee n   b r id g ed   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 o b tain ed   r esu l ts   w er to   i m p r o v e   t h 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 a m b i g u i t y   a n d   er r o r ,   im p r o v ed   th 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 au th o r s   w o u ld   li k to   th a n k   th 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 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 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 &   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     u sin g   l o g ica a p p r o a c h ,"   In ter n a ti o n a J o u rn a o S o ft wa re   E n g i n e e rin g   a n d   it 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 &   P .   Ba n e rje e ,   " F o rm a 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 J o u rn a o 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 o w a rd a   F o rm a li z in g   U M L   Clas Dia g ra m   S e m a n ti c s , "   In   Pro c e e d in g o th e   Ne T re n d 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 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 &   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 S o lu ti o n   Ba se d   o n   Z , J o u rn a 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 M e th o d s   A re   Co n sid e re d   f o S a f e t y   Crit ica S y st e m s? ,"   J o u rn a o 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 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   No tatio n   f o 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 o f   S y ste m , "   In   Pro c e e d in g o f   In ter n a t io n a 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 sp e c if ic a ti o n   f o th e   in v e n to ry   s y ste m   u sin g   lan g u a g e ,"   In   Pro c e e d in g 4 th   In ter n a ti o n a 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 S p e c if i c a ti o n   f o 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 o I n ter n a ti o n a C o n fer e n c e   o n   Rec e n T re n d a n d   C h a ll e n g e 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 F ra m e w o rk   o f   T ra n s f o rm in g   In f o r m a Re q u irem e n ts  S p e c if ica ti o n   to   S p e c if ica ti o n ,"   In   Pro c e e d in g o 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 m e th o d s:  Be n e f it s,  c h a ll e n g e a n d   f u tu re   d irec ti o n , "   J o u rn a o Gl o b a 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 &   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:   m o ti v a ti o n   to   f o r m a m e th o d s , "   In   Pro c e e d in g In ter n a ti o n a Co n fer e n c e   fo Co n v e rg e n c e   o 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 m e th o d f o 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 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 o f   M o b il e   Cl o u d   A p p li c a ti o n u si n g   UML , "   In ter n a ti o n a J o u rn a o f   El e c trica 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 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 o El e c trica 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 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 M in istry   o f   Ed u c a ti o n ,   Na jaf ,   Ira q   . He 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 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 o Co m p u ter  S c ien c e   a Dire c to ra te  o 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 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 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.