I nte rna t io na 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.   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 Speci ficat io o Q o S   Neg o ti a tion i 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 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 (OD P w il se e   a n   in c re a sin g   o 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 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 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 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 u to   d e v e lo p   a   m o d e f o 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 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 m o d e l,   w e   d e v e lo p   it   u si n g   a   f o r m a m e th o d .   I n   o u r   c a se ,   w e   w il u se   Ev e n t - B   to   g e in   th e   e n d   o f   o u d e v e lo p m e n a   sy ste m   c o rre c 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 ©   2 0 1 7   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 :   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 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 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 s t r u ctu r o f   o r g a n izatio n s   h av led   to   th 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 d is tr ib u ted   s tr u ct u r es  w h o s co m p o n e n t s ,   b o th   h ar d w ar a n d   s o f t w ar e,   ar 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 co m p o n en t s   ar d e v elo p ed   b y   d i f f er en 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 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 to   h i g h l y   h eter o g e n eo u s   s y s te m s .   T h a p p licatio n s   t h at   s u p p o r 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 in ter ac tio n   b et w ee n   th e s ap p licatio n   co m p o n en ts   is   o n o f   t h asp ec ts   o f   th d is tr ib u ted   tr ea t m e n t.  Sp ec i f icall y ,   t h 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 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 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 co m m u n icatio n   b et w ee n   co m p o n e n ts   m a y   b 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 d ev elo p ed   ca r ef u ll y   d u 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   f o r m al  m et h o d   t o   en s u r 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   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 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 a n d   v er if ica tio n   o f   s o f t w ar an d   h ar d w ar s y s te m s   [ 4 ] .   T h er ar 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 Z ,   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 t h e   f o r m   o f   p r ed icate .   T h er is   also   B - m et h o d   w h ic h   is   m et h o d   o f   s o f t w ar d ev e lo p m en b ased   o n   B ,   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 m ac h i n n o tatio n ,   u s ed   in   th d ev elo p m e n o f   co m p u ter   s o f t w ar e.   I 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 w i ll  u s E v en t - B   [ 6 ]   s i n ce   it   allo w s   u s   to   p r o v th at   o u r   s y s te m   i s   co r r ec 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 d o n au to m atica ll y   b y   to o 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 w h ic h   m ea n s   cr ea tin g   an   ab s tr ac m o d el  an d   en r ich in g   it  i n   m u l tip le   s tep s   b y   ad d in g   m o r d etails  t o   g et  m o r co n cr ete  m o d el  [ 8 ] .   I n   ev er y   r ef in e m e n t,  w p r o v th at  t h s y s te m   is   co r r ec an d   it  d o es  n o co n tr ad ict  w i th   t h p r ev io u s   o n e,   w h er eb y   th r es u lti n g   s y s te m   i s   co r r ec 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 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 b e g i n n in g ,   w p r ese n t h 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 t h s y s te m   r eq u ir e m e n 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 s tr ateg y   th at   w w il u s 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 w o r k   d o n an d   o u r   ex p ec tatio n   ab o u f u tu r w o r k s .       2.   RE L AT E WO RK S   U s in g   E v e n B   to   Sp ec if y   Qo in   ODP   E n ter p r is L an g u a g e‖   [ 1 ]   lik 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   s p e cif ica tio n   f o r   th d if f er e n ac to r s   o f   t h s y s te m   an d   th eir   s tates  a n d   it  also   p r esen n eg o tia tio n   v a l u es.  Ho w ev er ,   it  d o esn p r esen 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 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 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 n eg o tiat io n ,   it  p r esen t s   g o o d   s p ec if icatio n   o f   th 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   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 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 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 n e g o tiatio n ‖  [ 1 0 ]   p r esen ts   a n   ex a m p le  o f   Qo n e g o tiatio n   ap p lied   to   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 m o d els  a n d   s tatis tics   r es u lt s .   T h s a m as t h p r ev io u s   p ap er ,   th er is   n o th i n g   p r o v in g   th co r r ec tn es s   o f   t h s y s te m .   Ou r   w o r k   i s   p r esen ti n g   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 th 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   m o d elin g   o f   n e g o tiatio n   in   m o r 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 AP P RO A CH   Qu alit y   o f   Ser v ice  ( Qo S)  is   m an a g e m en co n ce p 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 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 is   f u n d a m en ta 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 w i ll b ase  o u r   s t u d y   o n   t h tr ad er   co n ce p [ 1 ] .   T h is   m ea n s   th at  i n   ad d itio n   o f   th clie n a n d   s er v er s ,   w e   w ill  h av t h ir d   ac to r ,   it  is   th tr ad er .   T h tr a d er   is   p la y i n g   t h r o le  o f   co n tr o ller   w h o   i s   ab le  to   g et  th b est  Qo p o s s ib le  f o r   clien t.   I n   th b eg in n i n g ,   a   clien p r o p o s v alu o f   q u al it y   o f   s er v ice  P   to   th tr ad er ,   th tr ad er   m a y   m o d i f y   th Qo p r o p o s ed   b y   th e   clien o r   n o t,  a f ter   th a t h tr ad er   s en d   th v al u P   o f   Qo S   to   th s er v er ,   w h e n   t h s er v e r   g ets  t h r eq u ir e d   v alu it  m a y   eit h er   r ef u s th e   r eq u est  o r   m a y   p r o p o s th v alu th at  it  m a y   o f f er s ,   at  t h is   s ta g t h tr ad er   w il eit h er   m o d if y   t h v alu p r o p o s ed   b y   th s er v er   o r   r etu r n s   it  d ir ec tl y   to   t h clie n t,  if   t h clie n is   s ati s f ied   w it h   t h p r o p o s ed   v alu h a cc ep ts   it  o r   else  h r ef u s es  it ,   in   th i s   ca s t h 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 s a m w a y .   T h F ig u r e   1   b elo w   p r e s en t s   t h 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 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 th r eq u ir e m e n d o cu m e n co r r ec tl y ,   w p r ese n it  alo n g   t w o   m ain   ax e s .   T h f ir s 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 s ec o n d   d escr ib es  th e s 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 n v ir o n m en t " E NV" .   W 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 s y s te m   allo w s   f o r   t h n eg o tiat io n   o f   Qo S   b et w ee n   clien t a n d   o n o r   m o r 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 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 clie n a cc ep ts   th Qo o r   if   h r ef u s e s   it   FUN  2     E NV  2 : A   clie n t c an   b 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 clien ca n   o n l y   ac ce p n e g o tiatio n   i f   t h tr ad er   p r o p o s es a   v alu 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 v alu o f   Qo S o r   r ef u s es to   o f f er   th s er v ice.     th tr ad er     ca n   o n l y   r e f u s n eg o tiat io n   i f   all  t h e   s er v er s   r ef u s to   o f f er   an y   Qo o r   if   th clien t   r ef u s all  th 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 o r   r ef u s to   o f f er   an y   Qo S     T h v alu p r o p o s ed   b y   t h s er v er   is   al w a y s   le s s   th an   o r   eq u al  t h v al u g iv e n   b y   t h tr ad er   FUN  5     E NV  5 : v alu e s   o f   Qo S   ar al wa y s   p o s iti v e.     T h tr ad er   al w a y s   p r o p o s v alu e s   le s s   t h a n   o r   eq u al  th v alu p r o p o s ed   b y   t h clien t   FUN  6   T h clien p r o p o s th v al u e   h w a n t s ,   t h en   th e   tr ad er   s ee k s   t h b est   v a lu e   les s   t h an   o r   eq u al   to   t h at   v alu 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 p r es en o u r   r ef i n e m en s tr ate g y .   W s tar b y   cr ea tin g   a n   ab s tr ac m o d el  ( f i r s 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 w ill   en r ich   it  b y   ad d in g   m o r f u n ct io n   an d   en v ir o n m en a s s u m p ti o n s   ( s ec o n d   r ef i n e m e n a n d   th ir d   r ef in e m e n t) .   I n   m o r d etail s ,   h er 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 b eg in n in g ,   w p r esen t h 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 s y s te m   ( FU 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 in cl u d n e g o tiatio n   v al u es  a n d   h o w   t h ac to r s   m a y   ch a n g it   w h ile  n eg o tiat in g   w it h   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 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 b y   m o d eli n g   t h v ar io u s   s tates  o f   th s y s te m   ac to r s .   Her is   o u r   f ir s t c o n tex t o f   th f ir s t r e f i n e m en t :     I n   th is   co n tex w h ic h   is   th s t atic  p ar o f   r ef in e m e n t,  w d ef i n th s et  ST A T E   as  p ar ti tio n   o f   th e   all  t h 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 h av e   ca lled   ―w ait‖ t h is   s tate   is   t h i n itiali za tio n   s tate.   W p r esen t h d y n a m ic   p ar o f   t h f ir s r e f in e m en ( m ac h i n e) we   s tar t b y   th i n v ar ian t t h a t a r t h p r o p er ties   th at  m u s t b 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     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 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 d ef i n e   S_ s ( Ser v er   s tate)   as  an   ele m en o f   ST A T E   th at  is   n o eq u al  ac ce p t,  th s a m g o   f o r   T _ s ( T r a d e r   s tate)   as   t h s er v er   a n d   t h tr a d er   ar n o allo w ed   to   ac ce p th n e g o tiatio n ,   th e   clien is   t h o n l y   ac to r   th at  m a y   ac ce p th n e g o tiatio n   t h i s   is   w h y   C _ s m a y   b 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 th at  co n tr o t h 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 clie n t   is   in   t h ac ce p s tate  th tr ad er   m u s b in   th s tate  p r o p o s ( in v 6 ) ,   w h ic h   m ea n   t h at  clien t   ca n n o ac ce p ts   a   n eg o tiat io n   i f   th tr ad er   d id   n o t p r o p o s es a   Qo S v alu e.   No w   w ca n   in i tialize  o u r   v ar iab le  w it h   ―w ait‖  v al u e.     B esid th in itializa tio n   ev e n t   w h a v m o r ev e n ts   t h at  ar ab le  to   ch an g t h s tate s   o f   th ac to r s   w h ile  p r eser v in g   all  t h i n v ar ian ts .   C lie n t_ p r o p o s e   is   th e v en th at  s tar ts   n e w   n eg o tia tio n w ca n   s tar a   n e w   n e g o tiatio n   o n l y   if   w e n d   th p r ev io u s   o n e,   w h ic h   m ea n s   t h at  t h tr ad er   is   n o t in   t h s tate  p r o p o s e‖ .     W h en   clien p r o p o s es  v alu o f   Qo S,  th 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 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 t r ad er   p r o p o s es.     T h o n ly   ca s w h er th tr ad er   w ill  r ef u s n e g o tiatio n   i s   w h e n   all  s er v er s   r ef u s n e g o t iatio n ,   an d   th en   t h 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 clien t r ef u s es a   n eg o tiat io n   if   h is   n o t sati s f ied   w i th   n e g o tiatio n   v al u p r o p o s ed   b y   t h 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 clien t is sat is f ied   w it h   t h p r o p o s ed   v alu b y   th tr ad er ,   h 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 p r ese n th n eg o tia tio n   v al u es.   A   clie n t p r o p o s v alu e   o f   q u alit y   o f   s er v ice   P   to   th tr ad er ,   th e   tr ad er   m a y   m o d i f y   t h Qo S   p r o p o s ed   b y   th 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 v al u P   o f   Qo to   t h s er v er ,   w h e n   t h e   s er v er   g e t h r eq u ir ed   v al u it   m a y   eit h er   r e f u s t h r eq u est  o r   m a y   p r o p o s th v al u th a it  is   ab le  to   o f f er ,   at  th i s   s ta g e   th tr ad er   w il eit h er   m o d if y   t h v al u p r o p o s ed   b y   t h s er v er   o r   r etu r n   it  d ir e ctl y   to   th clien t.  B ef o r m o d elin g   th ese  e v en t s ,   w p r ese n t   th co n tex b elo w   p r esen tin g   t h m a x i m u m   v al u o f   Qo S th at  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 h av n e w   v a r iab les  r ep r esen tin g   th 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 v a lu o f   Qo o f f er ed   in   ca s o f   ac ce p tin g   th n e g o tiatio n ) .   Mo r eo v er ,   w h a v e   ad d itio n al  in v ar ian f o r   th n e g o tiatio n s   v al u es :       Fu r t h er m o r e,   w r ef in t h e v en t s   o f   r ef i n e m e n 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 ac tio n s   s e ttin g   n eg o tiat io n   v a lu e s   t o   0   in   th in it ializatio n   ev e n t:     T h v alu p r o p o s ed   b y   th cli en t V clie n m u s t b 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     E X T E N D S       co n t ext   CO N S T A N T S     Vserver_ ma x     A X IO M S     a xm1:   Vserver_ ma     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        i n v8:   S _ st  =  p ro p o se    Vserver        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   a ct 4:   Vcl i en t       a ct 5:   Vserver    a ct 6:   Vt ra d er    a ct 7:   Vservi ce     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 2 0 1 7     2 0 4 5     2 0 5 3   2050     T h v alu p r o p o s ed   b y   th e   tr ad er   m u s t b p o s iti v n u m b er   less   th a n   o r   eq u al  t h v al u p r o p o s ed   b y   th clie n t.     s er v er   p r o p o s es  v al u e   le s s   t h a n   o r   eq u al   t h v al u p r o p o s ed   b y   t h 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  p r e d ef in ed   m ax i m u m   v al u o f   t h e   Qo s .     W h en   tr ad er   p r o p o s es  v al u o f   Qo S,  th e   s er v er   m a y   b u n ab le  to   o f f er   a n y   Qo S,   i n   t h is   ca s t h e   s er v er   r ef u s es t h p r o ce s s   o f   n eg o tiatio n .     I f   s er v er   r ef u s to   o f f er   Qo S ,   th 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   v alid   Qo S,  h o w e v er   i n   s o m ca s es   all  th s er v er s   ar u n ab le  to   o f f er Qo S,  w h ich   m ea n   t h at  t h tr ad er   w ill  s to p   n eg o tiat io n ,   w h ich   m ea n   th at  w r eset t h v a lu o f   Vtr ad er   an d   Vclien t to   0   in   t h ev e n t T r ad er _ r ef u s e:     E v en   i f   t h tr ad er   f in d   s er v e r   th at  m a y   o f f er   Qo s ,   th cl i en m a y   b n o s a tis f ied ,   in   t h is   ca s t h clien m a y   r e f u s t h n e g o tiati o n   b y   r esetti n g   all  t h n eg o tiat io n   v al u es to   0   in   t h ev e n t C li en t_ r ef u s e:     I n   th o t h er   h a n d ,   if   t h clie n is   s ati s f ied   w it h   th o f f er ed   Qo S ,   h m a y   ac ce p n e g o tiati o n .   I n   th i s   ca s e,   th v al u o f   s er v ice  w ill  b th v alu t h at  t h tr ad er   p r o p o s es,  w h ic h   m ea n s   th at  w h av o n ad d itio n al   ac tio n   in   t h ev e n 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     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        E N D   a ct 3:   Vt ra d er      a ct 4:   Vcl i en t     a ct 4:   Vcl i en t       a ct 5:   Vt ra d er      a ct 6:   Vserver      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 M u lt ipl S er v er s   I n   th is   las r ef in e m e n t,  w allo w   t h 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 clie n t g et s   t h Qo S v al u p r o p o s ed   h m a y   b n o t sati s f ie d   w it h   it a n d   r ef u s es t h n e g o t iatio n .   I n   t h is   ca s e,   th 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   b etter   Qo S.  T o   m o d el  th i s ,   w n ee d   to   d ef in e   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 co n tex t b elo w :     Si m i lar l y ,   w d ef i n n e w   t wo   v ar iab les.  T h f ir s v ar iab l is   s er v er   w h ich   r ep r esen t s   th cu r r en t   s er v er   t h at  w ar n eg o tia tin g   w i th .   T h 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 h a v n o t n e g o tiated   w i th   y et.   Mo r th a n   t h at ,   w h a v ad d itio n al  in v ar ia n t:     I n   th s a m w a y   a s   t h p r ev io u s   r ef i n e m en t,  w r ef i n also   th e v en ts   o f   m ac h i n 1 .   I n   th e   b eg in n i n g ,   w r ef in t h i n itia lizatio n   ev e n t:     I n   th 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 clie n p r o p o s es  Qo as  m e n tio n ed   b ef o r e,   at  th is   s tag e,   w i n itiate  t h s et  Ser v e r s _ No t_ T ested   as a ll th s er v e r s   o f   o u r   n et w o r k   i n   t h ev e n C lie n t_ p r o p o s :     T h tr ad er   is   th o n r esp o n s i b le  f o r   ch o o s in g   t h s er v er   to   n eg o tiate  w i th th i s   s er v er   is   c h o s f r o m   th 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 e m p t y   in   t h e v en t   T r a d er _ p r o p o s u s in g   t h 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   s er v er   f r o m   Ser v er s _ No t_ T ested :     W h en   s er v er   r ef u s e s   to   o f f er   Qo S,  w r e m o v i f r o m   Ser v er s _ No t_ T ested   to   en s u r th at  w e   w o n t   n eg o tiate   w it h   th e   s a m s e v er   o v er   a n d   o v er   ag ai n .   T h ac tio n   allo w i n g   r e m o v i n g   t h s er v er   f r o m   Ser v er s _ No t_ T ested   in   th ev en t Ser v er _ r ef u s i s   th f o llo win g:     T h 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 s er v er s   r e f u s to   o f f er   Qo w h ich   m e an   th at  w e   r e m o v ed   all  th 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 T r ad er _ r ef u s w il n ev er   b 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 b y   t h e   f o llo w in g   g u ar d :     T h clien ac ce p ts   th n e g o tia tio n   i f   t h er 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   Qo S   an d   th clie n t is  s atis f ied   w it h   it.  T h is   m ea n s   t h at  w w ill  h a v n e w   g u ar d   in   t h e v en 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 s e o f   ev id en ce   th at   en s u r e s   t h v al id it y   o f   th e   s y s te m ,   t h m o s 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 in v ar ian t   co n d itio n   b ef o r a n d   af ter   ea c h   ev e n t,  al th is   ca n   b d o n m an u all y .   Mo s t   o f   t h p r o o f s   ar ea s y   a n d   ar n o t   a ct 2:   Vservi ce    Vt ra d er    CO N T E X T     co n t ext     E X T E N D S       co n t ext   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 2 0 1 7     2 0 4 5     2 0 5 3   2052   t h k in d   o f   d e m o n s tr atio n s   t h at  co u ld   in ter est  m at h e m atic ian   b ec au s t h d if f ic u lt y   o f   m o d eli n g   i n   e v en t - is   n o t h co m p le x it y   o f   p r o o f   b u 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 h u g 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 all   th e   in v ar ia n t.  T h is   m ea n   t h at  t h p r o b le m   i s   t h at  t h a m o u n o f   p r o o f   to   p r o v is   v er y   b i g ,   in   o u r   c ase  w h av 2 1   i n v ar ian t s   ( 9   in   m ac h in 0 ,   1 0   i n   t h m ac h in 1   a n d   2   f o r   th e   m ac h in 2 )   an d   w h a v 1 0   ev en t s   t h is   m ea n   t h at  w h av 2 1 0   p r o o f   to   b e   d o n e.   L u ck i l y   th er is   p latf o r m   to   d o   th m o s 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 R o d in   p latf o r m   is   a n   I DE   b ased   o n   E clip s 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 s u p p o r f o r   r ef in e m e n a n d   m a th e m atica 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 clip s e   p latf o r m   an d   i s   m o r 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 ( A te lier ,   P r o B   . . . ) .   I n   th T ab le  1   b elo w   t h s tat is tic s   o f   p r o o f s   d o n 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 h a v d ev elo p ed   th p r o ce s s   o f   n eg o tiat io n   o f   Qo 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 h av p r o p o s ed   to   in tr o d u ce   d y n a m i tr ad in g   a s s i s ta n i n   t h u s er 's  ter m in al   to   h elp ,   f ir s tl y ,   to   ch o o s th 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 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 to   th u s er 's  r eq u ir e m e n t s   an d   ap p licatio n .   T h m o d el  w 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 in ter est  o f   t h 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 d esig n   o f   s y s te m   m o d els,  b u als o   in   its   r ef in e m e n t   p r in cip le  to   m aster   t h co m p l ex it y   o f   t h s y s te m   b y   p r o g r e s s i v a n d   s a f d e v elo p m e n t.  F o r   f u t u r w o r k s ,   w e   ar 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 lan d i n g   p r o ce s s w also   w ill  d ev e lo p   m o d el  o f   an   ab s tr ac t   co m p le x   ad ap tiv 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 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 fo a   S u sta in a b le  W o rld ,   IFI S e rie Ad v a n c e 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 e L a u re n V o i sin ,   T h e   E v e n t - M a th e m a ti c a 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 is  F o rm a 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   To o (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 Ja stra m   (Ed it o r)  F o re w o rd   b y   P r o f .   M ich a e 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 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 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 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 o f   Qo S   f o 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,   No v e Qo S   Ro u ti n g   A l g o rit h m   in   W ir e les 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 o f   El e c trica En g in e e rin g ,   Vo 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 a n d   A C 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 Qo S   Re q u irem e n ts  in   NG N ‖,   In ter n a t io n a J o u rn a o 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 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 S e m a n ti c   Ne t w o rk Ba se d   A p p ro a c h   f o 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 o E lec trica 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 se a u x   P o u Do n n é e Et c o m m u n ica ti o n   En tre  S y st è m e 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 c a n d id a te   a IIM CS   L a b o ra to ry   wh ich   sta n d f o 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 in   F a c u lt y   o f   Sc ien c e 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 c o m p lex   s y st e m 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 o f   h is  P h D.  h is  c u rre c 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 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 B a lo u k is  c u rre n tl y   a   p ro f e ss o o f   c o m p u ter  a n d   in f o rm a t io n   sc ien c e   a 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 a   P h 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 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 li b ra ry   (a a M a y   2 0 1 6 h e   h a se v e ra p u b li c a ti o n 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 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 o n   c o m p u ter  sc ien c e   a 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 M o ro c c o ).   S in c e   2 0 1 4 ,   h e   is  th e   Dire c to 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 Lab o ra to ry .   He   h a c o n d u c ted   m o re   th a n   ten P h t h e se 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 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 o f   th e   b e st  p a p e a w a rd a th e   IM P   S e s sio n   o f   IEE CI S T ’  2 0 1 6 .       Evaluation Warning : The document was created with Spire.PDF for Python.