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.   7 ,   No .   4 ,  A u g u s t   201 7 ,   p p .   2 0 4 5 ~ 2 0 5 3   I SS N:  2 0 8 8 - 8708 ,  DOI : 1 0 . 1 1 5 9 1 / i j ec e . v7 i 4 . p p 2 0 4 5 - 2053          2045       J o ur na l ho m ep a g e :  h ttp : //ia e s jo u r n a l.c o m/o n lin e/in d ex . p h p /I JE C E   For m a l  Speci ficat io n  o f  Q o S   Neg o ti a tion i n  O DP  Sys t e m       Abdes s a m a d J a rr a r,   Yo us s ef   B a lo uk i,  T a o ufiq G a d i   F a c u lt y   o f   S c ien c e s an d   T e c h n o l o g ies   In f o r m a ti c s,  I m a g in g   a n d   M o d e li n g   o f   Co m p lex   S y ste m s  L a b o ra to ry   S e tt a t,   M o ro c c o       Art icle  I nfo     AB ST RAC T     A r ticle  his to r y:   R ec eiv ed   Feb   9 ,   2 0 1 7   R ev i s ed   A p r   1 9 ,   2 0 1 7   A cc ep ted   Ma y   3 ,   2 0 1 7       T h e   f u tu re   o f   Op e n   Distrib u te d   P r o c e ss in g   s y ste m s  (OD P )  w il l  se e   a n   in c re a sin g   o f  c o m p o n e n ts  n u m b e r,   th e se   c o m p o n e n ts  a re   sh a rin g   re so u rc e s .   In   g e n e ra l,   th e se   re so u rc e s  a re   o ff e rin g   so m e   k in d   o f   se rv ice s.  Du e   to   t h e   h u g e   n u m b e r  o f   c o m p o n e n ts,   it   is  v e r y   d iff icu lt   to   o ff e r  th e   o p ti m u m   Qu a li t y   o f   se r v ice   (Qo S ).   T h is  e n c o u ra g e s  u s  to   d e v e lo p   a   m o d e l  f o r  Qo S   n e g o ti a ti o n   p ro c e ss   to   o p ti m ize   th e   Qo S   in   a n   OD P   sy ste m .   In   su c h   s y ste m ,   th e re   is  a   Hig h   risk   o f   so f t w a re   o r  h a rd w a r e   fa il u re .   T o   e n su re   g o o d   p e rf o r m a n c e   o f   a   s y ste m   b a s e d   o n   o u r  m o d e l,   w e   d e v e lo p   it   u si n g   a   f o r m a l  m e th o d .   I n   o u r   c a se ,   w e   w il l  u se   Ev e n t - B   to   g e t  in   th e   e n d   o f   o u r  d e v e lo p m e n t  a   sy ste m   c o rre c t  b y   c o n stru c ti o n .   K ey w o r d :   E v en t - B   F o r m al  m e th o d   Neg o tiatio n   ODP   Qu alit y   o f   s er v ice   R ef i n e m e n t p r o ce s s u s   Co p y rig h t  ©   2 0 1 7   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 :   A b d ess a m ad   J ar r ar ,    Facu lt y   o f   Sc ien ce s   an d   T ec h n o lo g ies,   C o m p u tin g ,   I m a g i n g   a n d   Mo d elin g   o f   C o m p lex   S y s te m s   L a b o r ato r y ,   FS T   Settat,  K m   3 ,   B . P .   :  5 7 7   R o u te  d e  C asab la n ca ,   Mo r o cc o .   E m ail:  A b d ess a m ad . j ar r ar @ g m ail. co m     1.   I NT RO D UCT I O N   T h e  ev o lu tio n   o f   te leco m m u n icatio n s   tec h n o lo g y   a n d   th e  s t r u ctu r e  o f   o r g a n izatio n s   h av e  led   to   th e  e m er g e n ce   o f   co m p le x   d is tr ib u ted   s y s te m s .   T h ese  s y s te m s   a r e  d is tr ib u ted   s tr u ct u r es  w h o s e  co m p o n e n t s ,   b o th   h ar d w ar e  a n d   s o f t w ar e,   ar e  o f   d if f er en t   t y p e s .   I n   s o m e   s y s te m s ,   th e s e  co m p o n en t s   ar e  d e v elo p ed   b y   d i f f er en t  ac to r s   ac tin g   in d ep en d e n tl y   o f   ea c h   o t h er .   T h e  as s e m b ly   o f   s u c h   co m p o n en t s   g i v es   r is e  to   h i g h l y   h eter o g e n eo u s   s y s te m s .   T h e  a p p licatio n s   t h at   s u p p o r t  th ese   s y s te m s   ar e   th e m s elv e s   co m p o s ed   o f   d is tr ib u ted   co m p o n e n t s .   T h e  in ter ac tio n   b et w ee n   th e s e  ap p licatio n   co m p o n en ts   is   o n e  o f   t h e  asp ec ts   o f   th e  d is tr ib u ted   tr ea t m e n t.  Sp ec i f icall y ,   t h e  d i s tr ib u ted   p r o ce s s i n g   co r r esp o n d   to   d if f er en t  asp ec t s   o f   in f o r m atio n   p r o ce s s in g   in   w h ic h   s p ec i f ic  co m p o n e n t s   ca n   b e  lo ca te d   in   d if f er en t   p lace s ,   d u r i n g   th i s   p r o ce s s   t h e  co m m u n icatio n   b et w ee n   co m p o n e n ts   m a y   b e  d elay s   o r   f ail u r es.  T h is   m ea n s   th at  t h is   k i n d   o f   s y s te m s   n ee d s   to   b e  d ev elo p ed   ca r ef u ll y   d u e  to   it s   co m p le x i t y   [ 1 ] .   T h is   m o ti v ate s   u s   to   m o d el  it  u s i n g   a  f o r m al  m et h o d   t o   en s u r e  t h e   co r r ec tn ess   o f   o u r   s y s te m   a n d   o b tain   a  v er y   s tr o n g   as s u r an ce   o f   b u g ’ s   ab s e n ce .   Fo r m al  m et h o d s   ar e  a  p ar ticu lar   k in d   o f   m at h e m a ticall y   b ased   tec h n i q u es   f o r   th e   s p ec i f icatio n   [ 2 ] ,   [ 3 ] ,   d ev elo p m e n t  a n d   v er if ica tio n   o f   s o f t w ar e  an d   h ar d w ar e  s y s te m s   [ 4 ] .   T h er e  ar e  a  v ar iet y   o f   f o r m al   m e th o d s   s u c h   as  lan g u ag e  Z ,   a  s p ec if icatio n   in   Z   i s   a   p r ed icate ,   th e   s p ec i f icatio n   o f   i n v ar ian ts   an d   th e   s p ec i f icatio n   o f   o p er atio n s   h a v e  t h e   f o r m   o f   a  p r ed icate .   T h er e  is   also   B - m et h o d   w h ic h   is   a  m et h o d   o f   s o f t w ar e  d ev e lo p m en t  b ased   o n   B ,   a  to o l - s u p p o r ted   f o r m al  m et h o d   b a s ed   o n   an   ab s tr ac t  m ac h i n e  n o tatio n ,   u s ed   in   th e  d ev elo p m e n t  o f   co m p u ter   s o f t w ar e.   I t  w as o r ig i n all y   d ev elo p ed   b y   J ea n - R a y m o n d   A b r i al  [ 5 ] .   I n   t h is   p ap er ,   w e  w i ll  u s e  E v en t - B   [ 6 ]   s i n ce   it   allo w s   u s   to   p r o v e  th at   o u r   s y s te m   i s   co r r ec t  b y   co n s tr u ct io n   b asi n g   o n   p r o o f s   o b lig atio n s .   T h ese  p r o o f s   ar e  d o n e  au to m atica ll y   b y   a  to o l  ca lled   R o d in   [ 7 ] .   E v en t - B   is   also   b ased   o n   r ef in e m e n t  w h ic h   m ea n s   cr ea tin g   an   ab s tr ac t  m o d el  an d   en r ich in g   it  i n   a  m u l tip le   s tep s   b y   ad d in g   m o r e  d etails  t o   g et  a  m o r e  co n cr ete  m o d el  [ 8 ] .   I n   ev er y   r ef in e m e n t,  w e  p r o v e  th at  t h e  s y s te m   is   co r r ec t  an d   it  d o es  n o t  co n tr ad ict  w i th   t h e  p r ev io u s   o n e,   w h er eb y   th e  r es u lti n g   s y s te m   i s   co r r ec t  b y   Evaluation Warning : The document was created with Spire.PDF for Python.
                      I SS N :   2 0 8 8 - 8708   I J E C E     Vo l.  7 ,   No .   4 ,  A u g u s t  2 0 1 7   :    2 0 4 5   –   2 0 5 3   2046   co n s tr u ct io n   [ 6 ] .   I n   th e  b e g i n n in g ,   w e  p r ese n t  t h e  p r o p o s ed   n eg o tia tio n   ap p r o ac h ,   th i s   ap p r o ac h   is   b ased   o n   tr ad er .   T h en ,   w e   d ef i n e  t h e  s y s te m   r eq u ir e m e n t  a lo n g   t w o   ax es :  F UN  a n d   E NV.   Af ter   t h at,   w e   p r esen t   o u r   r ef in e m e n t  s tr ateg y   th at   w e  w il l  u s e  a f ter   th at   to   s p ec i f y   o u r   s y s te m .   L a s tl y ,   w e   en d   th i s   p ap er   w it h   a   co n clu s io n   p r esen tin g   a n   ab s tr ac t a b o u t th e  w o r k   d o n e  an d   o u r   ex p ec tatio n   ab o u t  f u tu r e  w o r k s .       2.   RE L AT E D  WO RK S   ― U s in g   E v e n t  B   to   Sp ec if y   Qo S  in   ODP   E n ter p r is e  L an g u a g e‖   [ 1 ]   lik e  o u r   w o r k ,   is   s p ec i f y in g   Qo S   n eg o tiat io n   u s i n g   ev e n t - B ,   it  p r esen ts   a  s p e cif ica tio n   f o r   th e  d if f er e n t  ac to r s   o f   t h e  s y s te m   an d   th eir   s tates  a n d   it  also   p r esen t  n eg o tia tio n   v a l u es.  Ho w ev er ,   it  d o esn ’ t  p r esen t  a  s p ec if icat io n   o f   h o w   t h e   s y s te m   ac ts   e x ac tl y   s u c h   as  h o w   t h e  s y s te m   i s   ab le  to   n eg o tiate  w it h   m u l tip le  s er v er s .   ― E n d - to - en d   Qo S  n e g o tiatio n   in   n et w o r k   f ed er atio n s ‖  [ 9 ]   is   an o th er   w o r k   p r esen tin g   Qo S  n eg o tiat io n ,   it  p r esen t s   a  g o o d   s p ec if icatio n   o f   th e  n e g o tiatio n   p r o ce s s ,   an d   in   ad d itio n   it  p r esen t s   a  m at h e m a tical  m o d elin g .   Yet,   m at h e m atica l   m o d el  d o es n ’ t   p r o v e  th at   th e   s p ec i f icatio n   is   co r r ec t.  A ls o ,   i t   li m it s   t h e  s t u d y   i n   telec o m m u n icatio n   d o m a in .   ―An   ex a m p le  o f   d y n a m ic  Qo S  n e g o tiatio n ‖  [ 1 0 ]   p r esen ts   a n   ex a m p le  o f   Qo S  n e g o tiatio n   ap p lied   to   a  v id eo   s tr ea m i n g   ap p licatio n ,   th is   ex a m p le  is   p r esen ted   w it h   m at h e m atica l  m o d els  a n d   s tatis tics   r es u lt s .   T h e  s a m e  as t h e  p r ev io u s   p ap er ,   th er e  is   n o th i n g   p r o v in g   th e  co r r ec tn es s   o f   t h e  s y s te m .   Ou r   w o r k   i s   p r esen ti n g   a  f o r m al  s p ec if icatio n   u s i n g   E v en t - B ,   th is   allo w s   u s   to   en s u r e  th e  c o r r ec tn ess   o f   o u r   s y s te m   u s in g   p o o f   o b lig atio n s ,   it  al s o   p r esen t s   a  m o d elin g   o f   n e g o tiatio n   in   m o r e  d etails.  A ls o ,   o u r   w o r k   i s   p r o v ed   u s i n g   R o d in   p l atf o r m   [ 7 ]   w h ic h   av o id   h u m an   m is ta k es d u r in g   p r o v in g   p r o o f   o b lig atio n s .       3.   NE G O T I AT I O N  AP P RO A CH   Qu alit y   o f   Ser v ice  ( Qo S)  is   a  m an a g e m en t  co n ce p t  th at  ai m s   to   o p ti m ize  n et w o r k   r e s o u r ce s   o r   p r o ce s s   an d   en s u r e  g o o d   p er f o r m a n ce   o f   an   Op en   Dis tr ib u ted   P r o ce s s in g   ( ODP )   s y s te m ,   th i s   co n ce p t  is   f u n d a m en ta l  in   m an y   f ield s   s u ch   as  tr an s m is s io n   p r o to co ls   [ 1 1 ] ,   r o u tin g   al g o r it h m s   [ 1 2 ] ,   r eso u r ce s   allo ca tio n   alg o r ith m s   [ 1 3 ]   an d   w eb   s er v i ce   [ 1 4 ] .   I n   o u r   n eg o tiatio n   p r o ce s s ,   w e  w i ll b ase  o u r   s t u d y   o n   t h e  tr ad er   co n ce p t  [ 1 ] .   T h is   m ea n s   th at  i n   ad d itio n   o f   th e  clie n t  a n d   s er v er s ,   w e   w ill  h av e  a  t h ir d   ac to r ,   it  is   th e  tr ad er .   T h e  tr a d er   is   p la y i n g   t h e  r o le  o f   a  co n tr o ller   w h o   i s   ab le  to   g et  th e  b est  Qo S  p o s s ib le  f o r   a  clien t.   I n   th e  b eg in n i n g ,   a   clien t  p r o p o s e  a  v alu e  o f   q u al it y   o f   s er v ice  P   to   th e  tr ad er ,   th e  tr ad er   m a y   m o d i f y   th e  Qo S  p r o p o s ed   b y   th e   clien t  o r   n o t,  a f ter   th a t  t h e  tr ad er   s en d   th e  v al u e  P ’   o f   Qo S   to   th e  s er v er ,   w h e n   t h e  s er v e r   g ets  t h e  r eq u ir e d   v alu e  it  m a y   eit h er   r ef u s e  th e   r eq u est  o r   m a y   p r o p o s e  th e  v alu e  V  th at  it  m a y   o f f er s ,   at  t h is   s ta g e  t h e  tr ad er   w il l  eit h er   m o d if y   t h e  v alu e  p r o p o s ed   b y   th e  s er v er   o r   r etu r n s   it  d ir ec tl y   to   t h e  clie n t,  if   t h e  clie n t  is   s ati s f ied   w it h   t h e  p r o p o s ed   v alu e  h e  a cc ep ts   it  o r   else  h e  r ef u s es  it ,   in   th i s   ca s e  t h e  tr ad er   w ill  au to m at icall y   s tar t   n eg o tiat io n   w it h   a n o th er   s er v er   an d   p r o ce ed   in   t h e  s a m e  w a y .   T h e  F ig u r e   1   b elo w   p r e s en t s   t h e  p r o ce s s   o f   n eg o tiat io n   w it h   a   s er v er   b asi n g   o n   a   UI T   f o r m   [ 1 5 ]:         Fig u r e  1 .   Neg o tiatio n   P r o ce s s   [ 1 ]       4.   F O RM AL   SPECI F I CA T I O N   O F   Q O S NE G O CI AT I O N   4 . 1 .   Require m e nt  Do cu m ent   T o   p r esen t  th e  r eq u ir e m e n t  d o cu m e n t  co r r ec tl y ,   w e  p r ese n t  it  alo n g   t w o   m ain   ax e s .   T h e  f ir s t  a x i s   ex p r ess es   th e   m ain   f u n ctio n s   o f   s y s te m   " FUN" ,   an d   t h e  s ec o n d   d escr ib es  th e s e  f u n ct io n s   an d   p r o v id es  s o m e   d etails r eg ar d in g   th e  e n v ir o n m en t " E NV" .   W e  p r esen t o u r   r e q u ir e m e n t d o cu m en t a s   f o llo ws:     T h e  s y s te m   allo w s   f o r   t h e  n eg o tiat io n   o f   Qo S   b et w ee n   a  clien t a n d   o n e  o r   m o r e  s er v er s   FUN  1     Evaluation Warning : The document was created with Spire.PDF for Python.
I J E C E     I SS N:  2 0 8 8 - 8708       F o r ma l S p ec ifica tio n   o f Q o S   N eg o tia tio n   in   ODP   S ystem  ( A b d ess a ma d   Ja r r a r )   2047   E NV  1 : T h e  tr ad e r   is   an   in ter m ed iate  b et w ee n   clie n t a n d   s e r v er .     Neg o tiatio n   e n d   if   t h e  clie n t  a cc ep ts   th e  Qo S  o r   if   h e  r ef u s e s   it   FUN  2     E NV  2 : A   clie n t c an   b e  i n   o n e   o f   th r ee   s tate s   ( p r o p o s e,   ac ce p t o r   r ef u s e) .     T h e  clien t  ca n   o n l y   ac ce p t  n e g o tiatio n   i f   t h e  tr ad er   p r o p o s es a   v alu e  o f   q u alit y   o f   s er v ice   FUN  3     E NV  3 : A   tr ad er   ca n   eith er   p r o p o s e  a  v alu e  o f   Qo S o r   r ef u s es to   o f f er   th e  s er v ice.     th e  tr ad er     ca n   o n l y   r e f u s e  n eg o tiat io n   i f   all  t h e   s er v er s   r ef u s e  to   o f f er   an y   Qo S  o r   if   th e  clien t   r ef u s e  all  th e  p r o p o s ed   v alu es  o f   Qo S   FUN  4     E NV  4 : a   s er v er   ca n   p r o p o s e  o r   r ef u s e  to   o f f er   an y   Qo S     T h e  v alu e  p r o p o s ed   b y   t h e  s er v er   is   al w a y s   le s s   th an   o r   eq u al  t h e  v al u e  g iv e n   b y   t h e  tr ad er   FUN  5     E NV  5 : v alu e s   o f   Qo S   ar e  al wa y s   p o s iti v e.     T h e  tr ad er   al w a y s   p r o p o s e  v alu e s   le s s   t h a n   o r   eq u al  th e  v alu e  p r o p o s ed   b y   t h e  clien t   FUN  6   T h e  clien t  p r o p o s e  th e  v al u e   h e  w a n t s ,   t h en   th e   tr ad er   s ee k s   t h e  b est   v a lu e   les s   t h an   o r   eq u al   to   t h at   v alu e  i n   all  s er v er s   FUN7     4 . 2 .   Ref ine m ent   S t ra t eg y   Af ter   s p ec i f y i n g   o u r   n e g o tiati o n   p r o ce s s   co r r ec tly ,   w e  p r es en t  o u r   r ef i n e m en t  s tr ate g y .   W e  s tar t  b y   cr ea tin g   a n   ab s tr ac t  m o d el  ( f i r s t  r ef i n e m e n t)   co n tai n i n g   th e   p r in cip al  f u n ctio n s   o f   o u r   s y s te m ,   t h e n   w e  w ill   en r ich   it  b y   ad d in g   m o r e  f u n ct io n   an d   en v ir o n m en t  a s s u m p ti o n s   ( s ec o n d   r ef i n e m e n t  a n d   th ir d   r ef in e m e n t) .   I n   m o r e  d etail s ,   h er e  is   o u r   r ef in e m en t stra te g y :   a.   First  r ef i n e m e n t:  I n   th e  b eg in n in g ,   w e  p r esen t  t h e  v ar io u s   ac to r s   s tates  ( clien t,  tr ad er   an d   s er v er s )   an d   th e   b asic lo g ic  o f   t h e  s y s te m   ( FU N  1 ,   FUN  2 ,   FUN  3 ,   FUN  4 ,   E NV  1 ,   E NV  2 ,   E NV  3   an d   E NV  4 )   b .   Seco n d   r ef in e m e n t:  in   t h i s   r ef in e m e n t,  w e  in cl u d e  n e g o tiatio n   v al u es  a n d   h o w   t h e  ac to r s   m a y   ch a n g e  it   w h ile  n eg o tiat in g   w it h   a  s er v e r   ( FUN  5 ,   E NV  5   an d   E NV  6 ) .   c.   T h ir d   r ef in e m en t: la s tl y ,   t h e   s y s te m   i s   ab le  to   n eg o tiate  w i th   m u lt ip le  s er v er s   ( FU N  7 ) .     4 . 3 .   F irst  Ref ine m ent :   Sp ec if y ing   Act o rs S t a t es   As  it  is   m e n tio n ed   b ef o r e,   w e   s tar t  b y   m o d eli n g   t h e  v ar io u s   s tates  o f   th e  s y s te m   ac to r s .   Her e  is   o u r   f ir s t c o n tex t o f   th e  f ir s t r e f i n e m en t :     I n   th is   co n tex t  w h ic h   is   th e  s t atic  p ar t  o f   a  r ef in e m e n t,  w e  d ef i n e  th e  s et  ST A T E   as  a  p ar ti tio n   o f   th e   all  t h e  p o s s ib le   s tate s   i n   th e   s y s te m   o f   a n   ac to r s .   I n   ad d itio n ,   w e   ad d   an   ad d itio n al  s tate  th at  w e  h av e   ca lled   ―w ait‖ ;  t h is   s tate   is   t h e  i n itiali za tio n   s tate.   W e  p r esen t  t h e  d y n a m ic   p ar t  o f   t h e  f ir s t  r e f in e m en t  ( m ac h i n e) ;  we   s tar t b y   th e  i n v ar ian t t h a t a r e  t h e  p r o p er ties   th at  m u s t b e  p r es er v ed   d u r in g   s y s te m   o cc u r r en ce :   C O N T E X T     c o nt e xt 0      S E T S     S T A T E     C O N S T A N T S     pr o po se       r e f us e       ac c e pt       wai t     A X IO M S     axm 1:par t i t i o n( S T A T E , {p r o po se }, {r e f us e },  {a c c e pt }, {wai t })   E N D   Evaluation Warning : The document was created with Spire.PDF for Python.
                      I SS N :   2 0 8 8 - 8708   I J E C E     Vo l.  7 ,   No .   4 ,  A u g u s t  2 0 1 7   :    2 0 4 5   –   2 0 5 3   2048     I n   th ese  i n v ar ian t s ,   w e  d ef i n e   S_ s t  ( Ser v er   s tate)   as  an   ele m en t  o f   ST A T E   th at  is   n o t  eq u al  ac ce p t,  th e  s a m e  g o   f o r   T _ s t  ( T r a d e r   s tate)   as   t h e  s er v er   a n d   t h e  tr a d er   ar e  n o t  allo w ed   to   ac ce p t  th e  n e g o tiatio n ,   th e   clien t  is   t h e  o n l y   ac to r   th at  m a y   ac ce p t  th e  n e g o tiatio n   t h i s   is   w h y   C _ s t  m a y   b e  eq u al  a n y   s tate.   I n   ad d itio n ,   w e   p r esen t   s o m e   i n v ar ia n t  th at  co n tr o l  t h e  p o s s ib le   s tate   c o m b i n atio n s ,   f o r   ex a m p le,   i f   th e  clie n t   is   in   t h e  ac ce p t  s tate  th e  tr ad er   m u s t  b e  in   th e  s tate  p r o p o s e  ( in v 6 ) ,   w h ic h   m ea n   t h at  a  clien t   ca n n o t  ac ce p ts   a   n eg o tiat io n   i f   th e  tr ad er   d id   n o t p r o p o s es a   Qo S v alu e.   No w   w e  ca n   in i tialize  o u r   v ar iab le  w it h   ―w ait‖  v al u e.     B esid e  th e  in itializa tio n   ev e n t   w e  h a v e  m o r e  ev e n ts   t h at  ar e  ab le  to   ch an g e  t h e  s tate s   o f   th e  ac to r s   w h ile  p r eser v in g   all  t h e  i n v ar ian ts .   C lie n t_ p r o p o s e   is   th e  e v en t  th at  s tar ts   a  n e w   n eg o tia tio n ;  w e  ca n   s tar t  a   n e w   n e g o tiatio n   o n l y   if   w e  e n d   th e  p r ev io u s   o n e,   w h ic h   m ea n s   t h at  t h e  tr ad er   is   n o t in   t h e  s tate  ― p r o p o s e‖ .     W h en   a  clien t  p r o p o s es  a  v alu e  o f   Qo S,  th e  tr ad er   s w itc h es  h is   s tate  to   ― p r o p o s e‖   to   s tar t n eg o tiat io n   w it h   s er v er s .     T h e  s er v er   p r o p o s es o r   r ef u s es   n eg o tiatio n   i f   an d   o n l y   if   t h e  t r ad er   p r o p o s es.     T h e  o n ly   ca s e  w h er e  th e  tr ad er   w ill  r ef u s e  n e g o tiatio n   i s   w h e n   all  s er v er s   r ef u s e  n e g o t iatio n ,   an d   th en   t h e  tr ad er   e n d s   n e g o tiatio n   an d   in f o r m s   clie n t.     T h e  clien t r ef u s es a   n eg o tiat io n   if   h e  is   n o t sati s f ied   w i th   n e g o tiatio n   v al u e  p r o p o s ed   b y   t h e  tr ad er .   VA R IA B LE S     S _ st       C _ st       T _ st     INVAR IA N T S     i nv 1:   S _ st   ∈   S T A T E       i nv 2:   S _ st  ≠  a c c e pt       i nv 3:   C _ st   ∈ S T A T E       i nv 4:   T _ st   ∈   S T A T E       i nv 5:   T _ st  ≠  a c c e pt       i nv 6:   C _ st  =  a c c e pt   ⇒   T _ st   =  p r o po s e       i nv 7:   T _ st  =  r e f us e   ⇒   C _ st  ≠  a c c e p t       i nv 8:   T _ st  =  r e f us e   ⇒   S _ st  =  r e f us e       i nv 9:   S _ st  =  p r o po se   ⇒   T _ st  =  p r o po s e     INI TI A L ISA TI O N:       T H E N       a ct 1:   S _ st   ≔   wa i t         a ct 2:   C_ st   ≔   wa i t         a ct 3:   T _ st   ≔   wa i t     E N D   C l i en t _ p r o p o s e:       W H E R E       g rd 1:   C_ st  =  wa i t         g rd 2:   T _ st  ≠  p ro p o se      T H E N       a ct 1:   C_ st   ≔   p ro p o se      E N D   Tr a d er _ p r o p o s e:       W H E R E       g rd 1:   C_ st  =  p ro p o se      T H E N       a ct 1:   T _ st   ≔ p ro p o se      E N D   Ser v er _ r efu s e:     W H E R E       g rd 1:         T _ st  =  p ro p o se    T H E N       a ct 1:         S _ st   ≔   ref u se    E N D   Tr a d er _ r efu s e:       W H E R E       g rd 1:   C_ st  =  p ro p o se        g rd 2:   S _ st  =  ref u se      T H E N       a ct 1:   T _ st   ≔   ref u se        a ct 2:   C_ st   ≔   ref u se      E N D   Evaluation Warning : The document was created with Spire.PDF for Python.
I J E C E     I SS N:  2 0 8 8 - 8708       F o r ma l S p ec ifica tio n   o f Q o S   N eg o tia tio n   in   ODP   S ystem  ( A b d ess a ma d   Ja r r a r )   2049     A l s o ,   if   t h e  clien t is sat is f ied   w it h   t h e  p r o p o s ed   v alu e  b y   th e  tr ad er ,   h e  ac ce p ts   n eg o tiatio n .       4 . 4 .   Seco nd   Ref ine m e nt:   M o delin g   Neg o t ia t io n V a lues   I n   t h is   r ef i n e m en t,   w e  p r ese n t  th e  n eg o tia tio n   v al u es.   A   clie n t p r o p o s e  a  v alu e   o f   q u alit y   o f   s er v ice   P   to   th e  tr ad er ,   th e   tr ad er   m a y   m o d i f y   t h e  Qo S   p r o p o s ed   b y   th e  clie n t   o r   m a y   k ee p   it,  a f ter   th at   th e   tr ad er   s en d   th e  v al u e  P ’   o f   Qo S  to   t h e  s er v er ,   w h e n   t h e   s er v er   g e t  t h e  r eq u ir ed   v al u e  it   m a y   eit h er   r e f u s e  t h e  r eq u est  o r   m a y   p r o p o s e  th e  v al u e  V  th a t  it  is   ab le  to   o f f er ,   at  th i s   s ta g e   th e  tr ad er   w il l  eit h er   m o d if y   t h e  v al u e  p r o p o s ed   b y   t h e  s er v er   o r   r etu r n   it  d ir e ctl y   to   th e  clien t.  B ef o r e  m o d elin g   th ese  e v en t s ,   w e  p r ese n t   th e  co n tex t  b elo w   p r esen tin g   t h e  m a x i m u m   v al u e  o f   Qo S th at  a  s er v er   m a y   o f f er   Vser v er _ m a x :     I n   m ac h in e1 ,   w e  h av e  n e w   v a r iab les  r ep r esen tin g   th e  n e g o t iatio n   v al u es  ( Vclie n t,  Vtr ad er ,   Vser v er   an d   Vser v ice  w h ich   is   t h e  v a lu e  o f   Qo S  o f f er ed   in   ca s e  o f   ac ce p tin g   th e  n e g o tiatio n ) .   Mo r eo v er ,   w e  h a v e   ad d itio n al  in v ar ian t  f o r   th e  n e g o tiatio n s   v al u es :       Fu r t h er m o r e,   w e  r ef in e  t h e  e v en t s   o f   r ef i n e m e n t  0   b y   ad d in g   ac tio n s   r esp o n s ib le  f o r   d ea lin g   w it h   Qo S v al u es s u c h   as th e s e  ac tio n s   s e ttin g   n eg o tiat io n   v a lu e s   t o   0   in   th e  in it ializatio n   ev e n t:     T h e  v alu e  p r o p o s ed   b y   th e  cli en t V clie n t  m u s t b e  a  n o t n u ll  n atu r al  n u m b er .   C l i en t _ r efu s e:       W H E R E       g rd 1:   C_ st  =  p ro p o se       g rd 2:   T _ st  =  p ro p o se      T H E N       a ct 1:   C_ st ≔   ref u se        a ct 2:   T _ st   ≔   ref u se        a ct 3:   S _ st ≔   ref u se      E N D   C l i en t _ a c c ep t :       W H E R E       g rd 1:   T _ st  =  p ro p o se      T H E N         a ct 1:   C_ st   ≔   a cc ep t        E N D   CO N T E X T     co n t ext 1      E X T E N D S       co n t ext 0    CO N S T A N T S     Vserver_ ma x     A X IO M S     a xm1:   Vserver_ ma x  ∈ ℕ     a xm2:   Vserver_ ma x >  0    E N D   INVAR IA N T S     i n v1:   Vcl i en t   ∈ ℕ     i n v2:   Vserver  ∈ ℕ     i n v3:   Vt ra d er  ∈ ℕ     i n v4:   Vservi ce  ∈ ℕ     i n v5:   Vcl i en t  ≥  Vt ra d er      i n v6:   Vt ra d er ≥  Vse rver      i n v7:   T _ st  =  p ro p o se  ⇔   Vt ra d er  ≠   0      i n v8:   S _ st  =  p ro p o se  ⇔   Vserver  ≠   0      i n v9:   ( C_ st  =  p ro p o se  ∨   C_ st  =  a cc ep t )   ⇔   V cl i en t   ≠   0       i n v10:   Vserver ≤  Vse r ver_ ma x    a ct 4:   Vcl i en t   ≔   0    a ct 5:   Vserver  ≔ 0    a ct 6:   Vt ra d er  ≔ 0    a ct 7:   Vservi ce ≔   0    Evaluation Warning : The document was created with Spire.PDF for Python.
                      I SS N :   2 0 8 8 - 8708   I J E C E     Vo l.  7 ,   No .   4 ,  A u g u s t  2 0 1 7   :    2 0 4 5   –   2 0 5 3   2050     T h e  v alu e  p r o p o s ed   b y   th e   tr ad er   m u s t b e  a  p o s iti v e  n u m b er   less   th a n   o r   eq u al  t h e  v al u e  p r o p o s ed   b y   th e  clie n t.     A  s er v er   p r o p o s es  a  v al u e   le s s   t h a n   o r   eq u al   t h e  v al u e  p r o p o s ed   b y   t h e  tr ad er ,   an d   t h i s   v a lu e   is   al w a y s   le s s   t h a n   o r   eq u al  a  p r e d ef in ed   m ax i m u m   v al u e  o f   t h e   Qo s .     W h en   a  tr ad er   p r o p o s es  a  v al u e  o f   Qo S,  th e   s er v er   m a y   b e  u n ab le  to   o f f er   a n y   Qo S,   i n   t h is   ca s e  t h e   s er v er   r ef u s es t h e  p r o ce s s   o f   n eg o tiatio n .     I f   a  s er v er   r ef u s e  to   o f f er   a  Qo S ,   th e  tr ad er   tr y   to   n eg o tiate   w it h   an o t h er   s er v er   u n til  it  f i n d   a  v alid   Qo S,  h o w e v er   i n   s o m e  ca s es   all  th e  s er v er s   ar e  u n ab le  to   o f f er Qo S,  w h ich   m ea n   t h at  t h e  tr ad er   w ill  s to p   n eg o tiat io n ,   w h ich   m ea n   th at  w e  r eset t h e  v a lu e  o f   Vtr ad er   an d   Vclien t to   0   in   t h e  ev e n t T r ad er _ r ef u s e:     E v en   i f   t h e  tr ad er   f in d   a  s er v e r   th at  m a y   o f f er   a  Qo s ,   th e  cl i en t  m a y   b e  n o t  s a tis f ied ,   in   t h is   ca s e  t h e  clien t  m a y   r e f u s e  t h e  n e g o tiati o n   b y   r esetti n g   all  t h e  n eg o tiat io n   v al u es to   0   in   t h e  ev e n t C li en t_ r ef u s e:     I n   th e  o t h er   h a n d ,   if   t h e  clie n t  is   s ati s f ied   w it h   th e  o f f er ed   Qo S ,   h e  m a y   ac ce p t  n e g o tiati o n .   I n   th i s   ca s e,   th e  v al u e  o f   s er v ice  w ill  b e  th e  v alu e  t h at  t h e  tr ad er   p r o p o s es,  w h ic h   m ea n s   th at  w e  h av e  o n e  ad d itio n al   ac tio n   in   t h e  ev e n t  C lie n t_ ac ce p t:   Clie nt _ p r op os e :       A N Y       va l     ›     W H E R E       …       g rd 3:   va l   ∈ ℕ       g rd 4:   va l  ≠  0      T H E N       a ct 1:   C_ st   ≔   p ro p o se        a ct 2:   Vcl i en t   ≔   va l       E N D   Tr a d er _ p r o p o s e:       A N Y       va l       W H E R E       g rd 1:   C_ st  =  p ro p o se        g rd 2:   va l   ∈ ℕ       g rd 3:   va l  ≤  Vcl i en t         g rd 4:   va l  ≥  Vse rver        g rd 5:   va l  ≠  0      T H E N       a ct 1:   T _ st   ≔ p ro p o se        a ct 2:   Vt ra d er  ≔   va l       E N D   Ser v er _ p r o p o s e:       A N Y       va l       W H E R E       g rd 1:   T _ st  =  p ro p o se        g rd 2:   va l   ∈ ℕ       g rd 3:   va l  ≤  Vt ra d er        g rd 4:   va l  ≠  0        g rd 5:   va l  ≤  Vse rver_ ma x      T H E N       a ct 1:   S _ st   ≔ p ro p o se        a ct 2:   Vserver  ≔   va l       E N D   Ser v er _ r efu s e:       W H E R E       g rd 1:   T _ st  =  p ro p o se      T H E N       a ct 1:   S _ st   ≔   ref u se        a ct 2:   Vserver  ≔   0      E N D   a ct 3:   Vt ra d er  ≔   0    a ct 4:   Vcl i en t ≔   0    a ct 4:   Vcl i en t   ≔   0    a ct 5:   Vt ra d er  ≔   0    a ct 6:   Vserver  ≔   0    Evaluation Warning : The document was created with Spire.PDF for Python.
I J E C E     I SS N:  2 0 8 8 - 8708       F o r ma l S p ec ifica tio n   o f Q o S   N eg o tia tio n   in   ODP   S ystem  ( A b d ess a ma d   Ja r r a r )   2051       4 . 5 .   T hird Re f i ne m ent :   Neg o t ia t io n w it h  M u lt ipl e  S er v er s   I n   th is   las t  r ef in e m e n t,  w e  allo w   t h e  s y s te m   to   n e g o tiate  w it h   m u ltip le  s er v er s .   I n   o th er   wo r d s ,   w h en   th e  clie n t g et s   t h e  Qo S v al u e  p r o p o s ed   h e  m a y   b e  n o t sati s f ie d   w it h   it a n d   r ef u s es t h e  n e g o t iatio n .   I n   t h is   ca s e,   th e  tr ad er   s tar ts   n eg o tia t in g   w i th   an o t h er   s er v er   th at  m a y   o f f er   a  b etter   Qo S.  T o   m o d el  th i s ,   w e  n ee d   to   d ef in e   a  s et  o f   s er v er s   in   o u r   s y s te m   i llu s tr ated   in   th e  co n tex t b elo w :     Si m i lar l y ,   w e  d ef i n e  n e w   t wo   v ar iab les.  T h e  f ir s t  v ar iab l e  is   s er v er   w h ich   r ep r esen t s   th e  cu r r en t   s er v er   t h at  w e  ar e  n eg o tia tin g   w i th .   T h e  s ec o n d   is   Ser v er s _ No t_ T ested   w h ich   r ep r ese n t s   th e   s et  o f   s er v er s   th at  w e  h a v e  n o t n e g o tiated   w i th   y et.   Mo r e  th a n   t h at ,   w e  h a v e  ad d itio n al  in v ar ia n t:     I n   th e  s a m e  w a y   a s   t h e  p r ev io u s   r ef i n e m en t,  w e  r ef i n e  also   th e  e v en ts   o f   m ac h i n e  1 .   I n   th e   b eg in n i n g ,   w e  r ef in e  t h e  i n itia lizatio n   ev e n t:     I n   th e  b e g in n i n g   o f   e v er y   n e w   n e g o tiatio n ,   t h e  clie n t  p r o p o s es  a  Qo S  as  m e n tio n ed   b ef o r e,   at  th is   s tag e,   w e  i n itiate  t h e  s et  Ser v e r s _ No t_ T ested   as a ll th e  s er v e r s   o f   o u r   n et w o r k   i n   t h e  ev e n t  C lie n t_ p r o p o s e  :     T h e  tr ad er   is   th e  o n e  r esp o n s i b le  f o r   ch o o s in g   t h e  s er v er   to   n eg o tiate  w i th ;  th i s   s er v er   is   c h o s e  f r o m   th e  s et  Ser v er s _ No t_ T ested ,   w h ic h   m ea n   t h at  w e   n ee d   t o   ch ec k   i f   t h is   s et   is   n o t  e m p t y   in   t h e  e v en t   T r a d er _ p r o p o s e  u s in g   t h e  f o ll o w i n g   g u ar d :     A l s o ,   th i s   ac tio n   p ick s   a  s er v er   f r o m   Ser v er s _ No t_ T ested :     W h en   a  s er v er   r ef u s e s   to   o f f er   a  Qo S,  w e  r e m o v e  i t  f r o m   Ser v er s _ No t_ T ested   to   en s u r e  th at  w e   w o n ’ t   n eg o tiate   w it h   th e   s a m e  s e v er   o v er   a n d   o v er   ag ai n .   T h e  ac tio n   allo w i n g   r e m o v i n g   t h e  s er v er   f r o m   Ser v er s _ No t_ T ested   in   th e  ev en t Ser v er _ r ef u s e  i s   th e  f o llo win g:     T h e  tr ad er   r ef u s es  n e g o tiatio n   if   an d   o n l y   i f   all  th e  s er v er s   r e f u s e  to   o f f er   a  Qo S  w h ich   m e an   th at  w e   r e m o v ed   all  th e  s er v er s   f r o m   Ser v er s _ No t_ T ested ,   th is   m ea n   th at  Ser v er s _ No t_ T ested   is   e m p t y .   T h is   m ea n s   th at  t h e  T r ad er _ r ef u s e  w il l  n ev er   b e  o cc u r r ed   u n les s   Ser v er s _ No t_ T ested   is   e m p t y ;  t h is   i s   d o n e  b y   t h e   f o llo w in g   g u ar d :     T h e  clien t  ac ce p ts   th e  n e g o tia tio n   i f   t h er e  is   a   s er v er   i n   Ser v er s _ No t_ T ested   th at  m a y   o f f er   a  Qo S   an d   th e  clie n t is  s atis f ied   w it h   it.  T h is   m ea n s   t h at  w e  w ill  h a v e  a  n e w   g u ar d   in   t h e  e v en t  C l ien t_ ac ce p t:         5.   P RO VIN G   SYS T E M   CO RRE CT NE S S   P r o o f   o b lig atio n s   ar e  a  s e t  o f   ev id en ce   th at   en s u r e s   t h e  v al id it y   o f   th e   s y s te m ,   t h e  m o s t  i m p o r tan t   a m o n g   t h e m   is   th e   p r eser v at io n   o f   i n v ar ian t s   p r o o f s   t h at   v alid ates   th e   p r eser v atio n   o f   all  th e  in v ar ian t   co n d itio n   b ef o r e  a n d   af ter   ea c h   ev e n t,  al l  th is   ca n   b e  d o n e  m an u all y .   Mo s t   o f   t h e  p r o o f s   ar e  ea s y   a n d   ar e  n o t   a ct 2:   Vservi ce  ≔   Vt ra d er    CO N T E X T     co n t ext 2      E X T E N D S       co n t ext 1    S E T S     S ervers     A X IO M S     a xm1:   S ervers ≠   ∅   E N D   i n v1:   server  ∈   S er vers    i n v2:   S ervers_ N o t _ T est ed   ∈ℙ ( S ervers)     INI TI A L ISA TI O N:       T H E N       …       a ct 8:   server  : ∈   S e rvers        a ct 9:   S ervers_ N o t _ T est ed   ≔   S ervers      E N D   a ct 4:   S ervers_ N o t _ T est ed   ≔   S ervers    g rd 6:   S ervers_ N o t _ T est ed  ≠   ∅   a ct 3:   server  : ∈   S e rvers_ N o t _ T est ed     a ct 3:   S ervers_ N o t _ T est ed   ≔   S ervers_ N o t _ T est ed   ∖ {server}    g rd 3:   S ervers_ N o t _ T est ed = ∅   g rd 2:   server  ∈   S er vers_ N o t _ T est ed     Evaluation Warning : The document was created with Spire.PDF for Python.
                      I SS N :   2 0 8 8 - 8708   I J E C E     Vo l.  7 ,   No .   4 ,  A u g u s t  2 0 1 7   :    2 0 4 5   –   2 0 5 3   2052   t h e  k in d   o f   d e m o n s tr atio n s   t h at  co u ld   in ter est  a  m at h e m atic ian   b ec au s e  t h e  d if f ic u lt y   o f   m o d eli n g   i n   e v en t - B  is   n o t  t h e  co m p le x it y   o f   p r o o f   b u t  d e m o n s tr atio n s   o f   co n s is te n c y   d esp ite  t h e  h u g e  n u m b er   o f   ev e n ts   a n d   in v ar ia n t s ,   all  e v e n ts   m u s t   p r eser v e  all   th e   in v ar ia n t.  T h is   m ea n   t h at  t h e  p r o b le m   i s   t h at  t h e  a m o u n t  o f   p r o o f   to   p r o v e  is   v er y   b i g ,   in   o u r   c ase  w e  h av e  2 1   i n v ar ian t s   ( 9   in   m ac h in e  0 ,   1 0   i n   t h e  m ac h in e  1   a n d   2   f o r   th e   m ac h in e  2 )   an d   w e  h a v e  1 0   ev en t s   t h is   m ea n   t h at  w e  h av e  2 1 0   p r o o f   to   b e   d o n e.   L u ck i l y   th er e  is   a  p latf o r m   to   d o   th e  m o s t  o f   t h ese  p r o o f s   au to m atica l l y ,   t h is   f r a m e w o r k   is   ca lled   R o d in .   T h e  R o d in   p latf o r m   is   a n   I DE   b ased   o n   E clip s e  f o r   E v e n t -   B   w h ic h   p r o v id es  e f f ec ti v e  s u p p o r t  f o r   r ef in e m e n t  a n d   m a th e m atica l  p r o o f .   T h e   p latf o r m   i s   o p en   s o u r ce ,   co n tr ib u tes  to   t h e  E clip s e   p latf o r m   an d   i s   m o r e  e x te n s ib le  w it h   p l u g g i n g   v er y   ef f ec tiv e  ( A te lier ,   P r o B   . . . ) .   I n   th e  T ab le  1   b elo w   t h e  s tat is tic s   o f   p r o o f s   d o n e  b y   R o d in :       T ab le  1 .   P r o o f   Statis tic s   El e me n t s   T o t a l   A u t o   man u a l   R e v i e w e d   U n d i sc h a r g e d   Q o sn e g o t   92   91   1   0   0   C o n t e x t 0   0   0   0   0   0   C o n t e x t 1   0   0   0   0   0   C o n t e x t 2   0   0   0   0   0   M a c h i n e 0   38   38   0   0   0   M a c h i n e 1   51   50   1   0   0   M a c h i n e 2   3   3   0   0   0       6.   CO NCLU SI O N   w e  h a v e  d ev elo p ed   th e  p r o ce s s   o f   n eg o tiat io n   o f   Qo S  b et w e en   o b j ec ts   in   an   ODP   s y s te m ,   u s in g   th e   tr ad in g   f u n ct io n .   W e  h av e  p r o p o s ed   to   in tr o d u ce   a  d y n a m i c  tr ad in g   a s s i s ta n t  i n   t h e  u s er 's  ter m in al   to   h elp ,   f ir s tl y ,   to   ch o o s e  th e  b est  s er v ice  p r o v id er   an d ,   s e co n d ly ,   to   d y n a m ica ll y   n eg o tiate  t h e  q u alit y   p ar a m eter s   o f   s er v ice  ( Qo S)  r esp o n s i v e  to   th e  u s er 's  r eq u ir e m e n t s   an d   ap p licatio n .   T h e  m o d el  w e  h a v e   d ev elo p ed   is   b ased   o n   th e   f o r m al  m et h o d   E v e n t - B .   T h e  in ter est  o f   t h e  E v en t - B   in   o u r   s t u d y   lies   in   its   m o d elin g   to   f o r m all y   ex p r ess   p r o p er ties   v alid ated   b y   e v id en ce   d u r i n g   t h e  d esig n   o f   s y s te m   m o d els,  b u t  als o   in   its   r ef in e m e n t   p r in cip le  to   m aster   t h e  co m p l ex it y   o f   t h e  s y s te m   b y   p r o g r e s s i v e  a n d   s a f e  d e v elo p m e n t.  F o r   f u t u r e  w o r k s ,   w e   ar e  w o r k i n g   o n   s p ec if y i n g   f o r m al l y   air cr a f t  lan d i n g   p r o ce s s ;  w e  also   w ill  d ev e lo p   a  m o d el  o f   an   ab s tr ac t   co m p le x   ad ap tiv e  s y s te m .       RE F E R E NC E S   [1 ]   Y.  Ba lo u k i   A ND   A l,   ― Us in g   Ev e n t  B  t o   S p e c ify   Qo S   in   OD P   E n t e rp rise   L a n g u a g e ‖,   Co ll a b o ra t ive   Ne two rk s  fo r  a   S u sta in a b le  W o rld ,   IFI P  S e rie s  Ad v a n c e s  in   I n fo rm a t io n   a n d   Co mm u n ica ti o n   T e c h n o lo g y ,   Vo l.   3 3 6 ,   p p .   4 7 8 - 4 8 5 ,   S p rin g e r,   2 0 1 0 .   [2 ]   Cristo p h e   M é tay e r  e t  L a u re n t  V o i sin ,   ― T h e   E v e n t - B  M a th e m a ti c a l  L a n g u a g e ‖ ,   M a rs 2 6   2 0 0 9 .   [3 ]   Big g s,  N,  ― Dis c re te  M a th e m a ti c s‖ M   S e c o n d   E d it i o n .   Ne w   De lh i:   Ox f o rd   Un iv e rsit y   P re ss ,   IS BN - 10:   0 1 9 8 5 0 7 1 7 8 ,   2 0 0 3 .   [4 ]   R.   W .   Bu tl e r , ― W h a t  is  F o rm a l  M e th o d s? ‖ ,   Re tri e v e d   2 0 0 6 - 11 - 16 ,  2 0 0 1 - 08 - 06 .   [5 ]   Je a n - Ra y m o n d   A b rial ,   ― T h e   B  To o l  (A b stra c t) ‖ ,   ( P DF) ,   I n   Ro b in   E.   Blo o m f ield   a n d   Ly n n   S .   M a r sh a ll   a n d   R o g e r   B.   Jo n e s.  V DM   —   T h e   W a y   Ah e a d ,   P r o c .   2 n d   V DM - Eu r o p e   S y m p o siu m .   L e c tu re   No tes   in   C o m p u ter  S c ien c e .   3 2 8 .   S p rin g e r.   p p .   8 6 – 8 7 .   IS BN  3 - 5 4 0 - 5 0 2 1 4 - 9.   1 9 8 8 .   [6 ]   Je a n - Ra y m o n d   A b rial ,  ― M o d e li n g   in   Ev e n t - B:   S y ste m   a n d   S o f twa re   De sig n ‖ ,   Ca m b rid g e   Un iv e rsit y   P re ss ,   2 0 0 8 .   [7 ]   M ich a e l  Ja stra m   (Ed it o r)  F o re w o rd   b y   P r o f .   M ich a e l  Bu t ler,  ― Ro d in   Us e r' s Ha n d b o o k ‖   ,   C o v e rs Ro d i n   v . 2 . 8 .   [8 ]   T h a i  S o n   Ho a n g ,   Hi r o n o b u   K u r u m a ,   Da v id   Ba sin ,   Je a n - Ra y m o n d   A b rial,   ―   De v e lo p i n g   T o p o l o g y   Dis c o v e r y   in   Ev e n t - B ‖,   2 0 0 9 .   [9 ]   He li a   P o u y ll a u ,   Rich a rd   Do u v il le,  ― En d - to - e n d   Qo S   n e g o ti a ti o n   in   n e tw o rk   f e d e ra ti o n s‖ ,   ICT   ET ICS   p ro jec t,   G ra n t   a g re e m e n t ,   F P 7 - 2 4 8 5 6 7   Co n trac t  Nu m b e r:  INFS O - ICT - 2 4 8 5 6 7 ,   2 0 1 0 .   [1 0 ]   P .   Cre m o n e se   ,   S . G io rd a n o ,   ― A n   e x a m p le o f   d y n a m ic Qo S   n e g o ti a ti o n ‖ ,   F in sie l   S . p . A   v ia M a tt e u c c i  3 4   P isa   Italy .   [1 1 ]   A u g u stin   WA Y AW O ,  ― T h e   T ra n sm issio n   M u lt ica st  a n d   T h e   Co n tro l  o f   Qo S   f o r  I P V6   Us in g   t h e   In sf ra stru c tu re   M P L S ‖ ,  In ter n a ti o n a l   J o u r n a l   o f   In fo rm a t io n   a n d   Ne two rk   S e c u rit y     ( IJ INS ) ,   V o l   1   N o   1 ,   p a g e s 9 - 2 7 .   2 0 1 2 .   [1 2 ]   L iu   Hu i,   ― A  No v e l  Qo S   Ro u ti n g   A l g o rit h m   in   W ir e les s  M e sh   Ne tw o rk s ‖ ,  T EL K OM NIKA   In d o n e s ia n   J o u rn a l  o f   El e c trica l  En g in e e rin g ,   Vo l  1 1   N o   3 ,   p a g e s 1 6 5 2 - 1 6 6 4 .   2 0 1 3 .   [1 3 ]   Da c - Nh u o n g   L e ,   ― P S O  a n d   A C O  A lg o rit h m s   A p p li e d   to   Op ti m iz a ti o n   Re so u rc e   A ll o c a ti o n   to   S u p p o r t  Qo S   Re q u irem e n ts  in   NG N ‖,   In ter n a t io n a l  J o u rn a l  o f  I n f o rm a ti o n   a n d   Ne two rk   S e c u rity  ( IJ INS ) ,   V o l   2   N o   3 ,   p a g e s  216 - 2 2 8 .   2 0 1 3 .   [1 4 ]   Na ji   Ha sa n . A . H,    Ga o   S h u ,     AL - G a b ri  M a le k   a n d     Jia n g   Zi - L o n g ,   ― A n   Op ti m a l  S e m a n ti c   Ne t w o rk Ba se d   A p p ro a c h   f o r  W e b   S e rv ice   Co m p o siti o n   w it h   Qo S ‖ ,   T EL KOM NIKA  In d o n e sia n   J o u rn a l  o f  E lec trica l  E n g i n e e rin g ,   V o l   1 1     No   8 ,   p a g e s 4 5 0 5 - 4 5 1 1 .   2 0 1 3 .   Evaluation Warning : The document was created with Spire.PDF for Python.
I J E C E     I SS N:  2 0 8 8 - 8708       F o r ma l S p ec ifica tio n   o f Q o S   N eg o tia tio n   in   ODP   S ystem  ( A b d ess a ma d   Ja r r a r )   2053   [1 5 ]   UIT - T ,   ― S é rie  X :  Ré se a u x   P o u r  Do n n é e s  Et c o m m u n ica ti o n   En tre  S y st è m e s  Ou v e rts,   T e c h n o lo g ies   d e   l' in f o rm a ti o n   –   Qu a li té  d e   se rv ice   –   G u id e   p o u r   les   m é th o d e s et   les   m é c a n is m e s Re c o m m a n d a ti o n ‖ ,   X 6 4 2   0 9 /1 9 9 8 .       B I O G RAP H I E S   O F   AUTH O RS       Abd e ss a m a d   J a r r a r   is  a   P h D  c a n d id a te   a t  IIM CS   L a b o ra to ry   wh ich   sta n d s  f o r  In f o rm a ti c s,  I m a g in g   a n d   M o d e li n g   o f   Co m p lex   S y st e m s  in   F a c u lt y   o f   Sc ien c e s  a n d   T e c h n o lo g ies   Ha ss a n   1 st  U n iv e rsity ,   S e tt a t,   M o ro c c o ,   h is  re se a rc h   i n tere sts  c e n ter  a ro u n d   m o d e li n g   o f  c o m p lex   s y st e m s  u sin g   fo rm a l   m e th o d s,  h e   is  c u rre n t ly   in   h is  se c o n d   y e a r  o f   h is  P h D.  h is  c u rre c t  r e se a rc h   f o c u s o n   m o d e li n g   a n   a b stra c t  c o m p l e x   a d a p ti v e   s y ste m ,   in   a d d i ti o n ,   h e   is  w o rk in g   o n   a   m e th o d   t o   so lv e   th e   p r o b lem   o f   in f in te  c y c les   in   c o m p lex   s y ste m s.         Yo u ss e f  B a lo u k i  is  c u rre n tl y   a   p ro f e ss o r  o f   c o m p u ter  a n d   in f o rm a t io n   sc ien c e   a t  th e   F a c u lt y   o f   S c ie n c e s   a n d   T e c h n o lo g ies ,   Ha ss a n   Ist   Un iv e rsit y ,   S e tt a t,   M o ro c c o .   He   h o ld s  a   P h D  in   Co m p u ter  S c ien c e   (2 0 1 0 )   f ro m   M o h a m m e d V   Un iv e rsit y ,   Ra b a t,   M o ro c c o   a n d   h e   g ra d u a te d   in   Co m p u ter  S c ien c e   (1 9 9 5 )  i n   Ca d i   Ay y a d   Un iv e rsit y ,   M a rr a k e c h ,   M o ro c c o   w h e re   h e   g o t  h is  M a ste r’s  d e g re e   in   c o m p u ter  S c ien c e .   A c c o rd in g   to   G o o g le  S c h o lar,  D BL P   d ig it a l  li b ra ry   (a s  a t  M a y   2 0 1 6 )  h e   h a s  se v e ra l  p u b li c a ti o n s  w h ich   ha v e   b e e n   c it e d   q u it e   a   f e w   ti m e s .   F in a ll y ,   h is  m a in   re s e a rc h   in tere sts  li e   in   th e   Da tab a se s,  Distrib u t e d   &   P a ra ll e l  C o m p u ti n g   a n d   S c ien ti f ic Co m p u ti n g .         G a d i   Ta o u fi q   is  a   P ro f e ss o r  o n   c o m p u ter  sc ien c e   a t  th e   f a c u lt y   o f   sc ien c e   a n d   tec h n o lo g ies   (Ha ss a n   F irst  Un iv e rsity   o f   S e tt a t  M o ro c c o ).   S in c e   2 0 1 4 ,   h e   is  th e   Dire c to r  o f   th e   In f o rm a ti c s,  I m a g in g   a n d   M o d e li n g   o f   Co m p lex   S y ste m s  Lab o ra to ry .   He   h a s  c o n d u c ted   m o re   th a n   ten s  P h D  t h e se s  a n d   w rit ten   a   f i f t y   o f   sc ien ti f ic  p a p e rs  in   th e   d o m a in   o f   3 D  m o d e ls  a n a l y sis,  m o d e ls  Driv in g   A rc h it e c tu re ,   Da ta m i n in g   a n d   Da tab a se   A n a l y sis,  M o d e li n g   o f   Co m p le x   S y ste m s.  He   is  re c ip ien t  o f   th e   b e st  p a p e r  a w a rd s  a t  th e   IM P   S e s sio n   o f   IEE E  CI S T ’  2 0 1 6 .       Evaluation Warning : The document was created with Spire.PDF for Python.