TELKOM NIKA , Vol.14, No .2, June 20 16 , pp. 734~7 4 0   ISSN: 1693-6 930,  accredited  A  by DIKTI, De cree No: 58/DIK T I/Kep/2013   DOI :  10.12928/TELKOMNIKA.v14i1.2732    734      Re cei v ed Se ptem ber 29, 2015; Revi se d Ja n uary 10,  2016; Accept ed Feb 3, 20 16   Property Analysis of Composable Web Services      Wei Liu*, Lu Wang, Yu y u e Du, Pin Wa ng, Chun Ya n  State Ke y  L a b o rator y  of Mini ng Dis aster Preventi on a nd C ontrol,    Shan do ng Un i v ersit y  of Sci e n c e and T e chno log y , Qing da o, Chin a   Coll eg e of Information Sci enc e and En gi neer ing, Sh a n d ong  Univers i t y   of Scienc e & T e ch nol og y,   Qingd ao, Ch in a   T he Ke y  La bor ator y   of Embed ded S y stem a n d  Serv ice C o m putin g, Minist r y  of Educatio n,    T ongji  Un iver sit y , Sha ngh ai,  Chin a   *Corres p o ndi n g  auther, e-ma i l : liu w e i_ doctor @ yea h .net       A b st r a ct   W eb services  are basic co mp on ents con s tructi ng a fle x ible  busi ness  process softw are. By   compos ing  mul t iple W eb s e rvi c es, a complic ated b u sin e ss process acr o ss  organ i z a t i on a nd de part m e n ts   can b e  for m e d . T h is p a p e r prese n t a for m a l   mo del  of  compos abl e  W eb servic es: co mpos ed s e rvic e   process  nets ( C SPNs). Prop erties  of Co mposa b le   W eb services are a naly z e d  bas ed   on CSPNs.  T h e   relati on betw e e n  a CSPN an d its correspo ndi ng W eb se rvic e process su bn ets are discuss ed. T he prop er ty   ana lysis  metho d s of CSP N s  a r e co me  u p  w i th. A dy na mic  p r operty  of CSP N s can  b e  d e te rmi ned  b a sed   on  static net structures by me a n s  of the propos e d  met hods.     Ke y w ords : pa ssing  mess age s, deadl ock-fre edo m,  bus in es s process, W eb services       Copy right  ©  2016 Un ive r sita s Ah mad  Dah l an . All rig h t s r ese rved .       1. Introduc tion  Service - o r ien t ed co mputin g (SO C ) i s   widely u s e d   [1]. With the  developm en t of Web   servi c e s , the  numbe r of  Web serv ices is in cre a si ng  dram atically  [ 2 -3]. Web  se rvice s  be co m e  a  basi c   comp o nent con s tru c ting a flexi b le bu sine ss pro c e ss. B y  compo s in g  multiple Web  servi c e s , a complicated b u sin e ss p r o c ess ca n be fo rmed [4 -5]. The appli c atio n of SOC re d u ce s  the complexi ty of busin e s s integ r atio n within  an  enterpri s e  or o r g anization an d a c ross  enterp r i s e s  o r  o r ga nizatio n s [6]. Se rvice-ori ented  computing  (S OC)  cha nge d the t r an ditiona l   softwa r e dev elopme n t. It  has be en u s ed in e-com m erce of across org ani zat i ons an d with in an   orga nization.   Different ente r pri s e s  or o r g anization s co ll aborate mut ually and form inter-e nterprise o r   inter-org ani za tion workflow. Whe n   colla boratio n h a p pen s am ong  enterpri s e s   or o r g ani zati on s  and diffe rent  depa rtment s  within a n  ent erp r ise or  org anization, a  workflo w  a c ross o r gani zat i ons  or  depa rtmen t s is ge ne rate d by m ean s  o f  intera ct ion s   [7-8]. Each o r gani zation  or  depa rtment i s   serve d  by a Web servi c e and this  Web  se rvice  serve a s  a  busin ess p r ocess am on g  orga nization s  or dep artme n ts within  a n  orga nization  [ 9 ].  Web   servi c e s   al so ca n be combi ned  by  many sm all  Web  se rvice s   within a n   enterp r i s e o r  a workflow amon g de p a rtment s of  an  enterp r i s e formed by intera ction s  of different  departments  [10]. In SOC  architec ture,  the  intera ction s  o r  collab o ratio n s a m on g dif f erent  e n terp rise s o r  de pa rtments a r e i m pleme n ted  by  me ss a g e  pas s i n g  amo ng W e b se r v ice s . By me ans  of me ssag e pa ssi ng,  Web  se rvice s  in  different ente r pri s e s  or d e partme n ts are con n e c ted  forming inte r-orga nizationa l Web service s   intera ction sy stem, which  l ead s  to We b servi c e  c o mpo s itio n ac r o ss  or g a n i za tion s .   W e b se r v ic e   comp ositio n is a impo rtant and valua b le  reserach field  in SOC [11].  To reali z e  Web  servi c e  compo s ition  effect ively,  many com p o s ition lang ua ges a n d   interface spec ific ations  are propos ed,  s u c h  as  WS -BPEL, WS-CDL and WS CI [12]. They   c an  be u s ed to d e scrib e  Web  servi c e  com p osition. Bu t they lack formal analy s is  for  We b service   composition.  Wheth e r  We b servi c e s  are comp osabl e or not  dep e nds o n  the proper exe c tion  of Web   servi c e  comp osition  workfl ow  acro ss o r gnization s.  If Web   servi c e comp ositio n workflo w  ca n   be  execute d  properly, Web  servi c e s  are com p o s ab le acro ss o r gnization s. If Web  servi c e   comp ositio n  workflo w   can not be exe c u t ed prope rly, Web  se rvices ar e not  com posable acro ss  Evaluation Warning : The document was created with Spire.PDF for Python.
TELKOM NIKA   ISSN:  1693-6 930       Prope rty Anal ysi s of Com p osa b le Web  Servi c e s  (We i  Liu)  735 orgni zatio n s.  Hen c e, to ensu r e Web service s   a r e compo s abl e, the pro p e r  exection of We b   servi c e co mp osition wo rkflow need   be   a nalysi z ed an d  verified. T h e re se arch i n  this a r e a  is p a id  more attention in SOC. We foc u s  on  and s t udy this  topic  in this  paper.   Web  servi c e  comp ositio n  workflo w  i s   o ften analy z ed  by formal  m e thod s in clu d i ng Petri   nets [13], stat e automato n   [14], descripti on logi c  [15],  pro c e ss  alge bra [16] a nd  so o n . Pro c e s s  algeb ra is  un intuitive for its exce ssive symbol i c  exp r essio n . For  descri p tion lo gic, mod e ling  a  servi c e  co mp osition  is  still  at a th eoretical l e ve l si nce it is comple x for de scri bi ng  servi c e s  a n d   analyzi ng the i r com p o s itio n. State automaton is in tu itive, but has less  mathe m atical a naly s is  method s. Ba sed  on thei r  strict mathe m a t ical defin itio n s  an d g r ap hical expression , Petri nets  are  an effective descriptio n  an d analysi s  tool for m odeli ng se rvice s  a nd fit for modeling dist ribut ed   and lo ose-co upled  syste m s like  Web   se rvice s . Hen c e ,  Petr nets are used to  mo del Web  se rvice   workflo w  and  Web  se rvice  comp ositio n workflo w  in this pap er.   In this pa pe r, the internal  pro c e s s of a  W eb  se rvice  i s  represente d  by a servi c e proce s s  net (SPN) ba sed o n  Petri nets. The inte ractio ns  a m o ng multiple Web se rvice s  a r e den oted b y  a  comp osed  se rvice p r o c e ss net (CSPN).  A CSPN i s   comp osed by  comm on p a ssi ng me ssa ge  places in  different SPNs.  The inte rface  passin g   me ssag e pla c e s  i n  a SPN indi cate the  pa ssing  messag es a m ong  We b service s . Th e  colla boration s  an d inte ra ctions a m on g  Web  se rvices are   r e pr es e n t ed  b y  C SPN s .     By CSPNs a nd SPNs,  We pre s e n t ne ce ssary  cond itions of prop er exe c ution  of Web   servi c e  co m positio n  workflow. By the s e  ne ce ssary con d ition s , imprope r  e x ecution  of  Web   servi c e  com p osition  ca n b e  judg ed. Even thou gh  e a c h of m u ltiple We b services i s  de adlo c k- free, a com p osition  workfl ow of multipl e  Web  se rvice s  is not certain to dea dlock-f r ee.  We   prop ose the   necesssary  condition  of th e p r ope r  exe c ution   of  a  co mpositio n wo rkflo w  of  mult iple  deadl ock-f r ee . We give the sub c la ss of Web  servi c e  comp sition. F o r the su bcl a ss, we give the  suffice nt an d  ne ce ssary  condition  of p r oper exe c utio n of  com p o s i t ion workflow. Differe nt fro m   previou s  m e thod s, these  method s p r e s ente d  in  thi s  pape r a r e b a se d on th e  static  stru cture of  CSPNs. By th ese meth od s, it is esay to  analyze p r op erties of com p o s abl e We b se rvice s .  The re st of this pap er i s  orga nized  as  follo ws. I n  Section 2,  Formal m o dels of  comp osable   Web  se rvices is p r e s ente d  and i n trod uc ed. We an alyze p r o pertie s  of co mpo s a b le   Web  se rvice s  in detail in Section 3. Sect ion 4 co ncl u d e s the pa per.     2. Formal Models of Co mposable Web Serv ices   Formal m ode ls are pro p o s ed for stu d ying t he sati sfied prope rties of compo s a b le We b   servi c e s . The  Web se rvice  pro c e ss n e ts are put  forwa r ded to den ote Web services. The intern al   servi c e proce s s  net s (ISPNs) are   raise d   to si gnify t he in ner  We b service  pro c e ss. A nd T h e   comp osed  Web  se rvice  pro c e s s net s (CSPNs)  are  pre s e n te d to express com p o s ed  Web   serv i c e s .    Defini tion 1:  A Web service is executed  prope rly i ff its input pa ssi ng messa g e s  can be   gotten and it can terminate  normally.   Defini tion 2 :   A compo s e d  We b  servi c e  is  executed  pr op erly iff e a ch  Web  se rvice in   comp osed se rvice is exe c u t ed prop erly.   A Web service pro c e ss  ca n be formally  rep r e s ente d  by a SPN   model.  Defini tion 3:   SPN  =( P ,  T ,  F ,  M 0 ) is a Web se rvice p r oce s s net wh ere   (1)  P  i s  a set of place s .  P = P I P MI P MO  are di sju n ct subsets of pla c e s , whe r e  P I  is a set   of internal pl ace s ,  P MI  is  a set of inpu t passing me ssage pl aces and  P MO  is  a set of outp u t   passin g  message pla c e s ;   (2)   P  inc l ud es tw o sp ec ia l in te r n a l  p l ac es :  i  and   o . Plac e  i  is a  sta r t  place:  • i = . Plac e  o  is  a end pla c e:  o • = ;  (3)  T  is a  set  of transition s  and  P T = .  t T ,  t  and  t  sepa ratel y  include s a internal   place at least ;     (4)  F ( P T ) ( T P ) are di rected e dge s repre s e n ting flow rel a tion s;  (5)  M :  P  is  the initial mark ing func tion of a SPN;  (6)  M 0 = [ i ], [ i ] ([ o ]) rep r e s ent s only pla c e  i  ( o )  contai n on e token;   (7)  x P I   T ,  x  is  on a  path from  i  to   o  an d  p P MI P MO .  x P MI ,  x=  a nd  x  onl y   in c l ud es  a   trans i tion.  x P Mo ,  x =  and  x  only incl ude s a   tran sition.   A com p o s ed  Web  service  pro c e s s com posed of  mult iple Web services  can  be formally  rep r e s ente d  by a CSPN m odel.   Evaluation Warning : The document was created with Spire.PDF for Python.
                             ISSN: 16 93-6 930   TELKOM NIKA   Vol. 14, No. 2, June 20 16 :  734 – 74 0   736 Defini tion 4:  Let  SPN k =( P k ,  T k ,  F k ,  M 0 k ) be a  SPN  of the  k -t h coo perative se rvice   pro c e ss net,  k  = 1 ,  2 , . . . , n .  CSPN  = ( P ,  T ,  F ,  M 0 ) is a compo s e d  Web  se rvice pro c e s s ne t   w h er e  1)  P = ∪ 1 ≤ k ≤ n P k ,  P = P I ∪ P MIO ∪ P CMI ∪ P CM O  are di sjun ct  sub s ets of pl aces, whe r e   P I = ∪ 1 ≤ k ≤ n P I k ,  P MIO =( ∪ 1 ≤ k ≤ n P MO k ) ( ∪ 1 ≤ k ≤ n P MI k )  P CMI = ∪ 1 ≤ k ≤ n P MI k \ ∪ 1 ≤ k ≤ n P MO k ,  P CMO = ∪ 1 ≤ k ≤ n P MO k \  ∪ 1 ≤ k ≤ n P MI k ;  2)  T  =  ∪ 1 ≤ k ≤ n T k ;  3)  F  =  ∪ 1 ≤ k ≤ n F k ;  .  4)  M :  P  is the marki ng functio n  of a SPN;  4)  M 0  is the initial marki n g, and  ∀ p ∈ P k :  M 0(p ) = M 0k(p) , k= 1, 2, . . .,n.  M ce   is the end  marking  whe r e each end pl ace  o  of  SPN k , k= 1, 2, . . .,n contai ns o n e  token.    In a  CSPN,   x P T  i s  call ed a  n ode. Its  pre s et  • x ={ y ( y , x )   F }, and  po stset   x • ={ y ( x , y ) F }.      Definition 5 :   Firing  rule s of a transitio n  t  in  CSPNs . In a  CSPN ,  t T ,  t  is enabled if  p • t ;  M ( p ) 1. Firing en abled  t  resul t s in a new markin g  M ′ :  p • t :  M ′ ( p )= M ( p )-1;  p t • :  M ′ ( p )= M ( p )+ 1;  R ( M 0 ) re pre s ent s the set  of all marki n g s  rea c h able from  M 0 .  Defini tion 6 :  A  CSP N  = ( P ,  T ,  F ,  M 0 ) is corre c t iff its corre s po ndi ng compo s e d  Web  servi c e is exe c uted p r op erl y .  Defini tion 7 :   If  CSPN  =  ( P ,  T ,  F ,  M 0 )  is   a C SPN co mpo s ed  o f   n   SPNs :   SP N k =( P k ,  T k ,  F k ,   M 0 k ),  k  = 1 ,  2 , . .  .,n , then  SPN k  is called t he We b se rv ice process subnet of  CSP N .  Defini tion 8 :  ISPN  =  ( IP ,  IT ,  IF ,  IM 0 ) is an inte rnal   net of  a  We b  se rvice  process net  SPN  = ( P ,  T ,  F ,  M 0 ), where   (1)  IP  is a set of place s .  IP = P I ;   (2)  IP  incl ude s two spe c ial  internal pl ace s :  i  and  o . Place  i  is a  start place:  • i = . Place  o   is an en d pla c e:  o • = ;  (3)  IT = T ;  (4)  IF = F (( P I T ) ( T P I ));   (5)  M :  IP   is the initial  markin g func tion of a ISPN;  IM 0 = [ i ];  M e = [ o ]   is th e en d  marking   whe r e the en d place  o  co n t ains on e token.  Firing rule s of transition s  in  ISPNs is the same a s  tho s e in   CSPNs .       3. Propert y   Analy s is of Compos able  Web Serv ic es   Suppo se e a ch input pa ssi ng me ssage  is ne ce ssary  for We b serv ice s . If a co mposed   Web  se rvice  can exe c ute  prop erly, then  each i nput  p a ssing m e ssa ge of ea ch  Web se rvice m u st   be gotten. Bu t each outp u t passin g  message of ea ch  Web  se rvice  doe s not hav e to be re ceiv ed   by anothe r  Web servi c e b e c au se  output  passin g  me ssage s do es no t affect the p r oper exe c utio n   of a compo s e d  Web  se rvice. So  the below theo rem  can be obtai ne d.  Theorem 1 :   If a compo s e d  Web  servi c e is execut e d  prop erly, then its co rrespondi ng   CSPN  =  ( P ,  T ,  F ,  M 0 ) sat i sf ies:   P CMI = .  Proof : If a composed Web  service ca n execute  p r op erly, it means that every passi n g   messag e of e a ch  We b se rvice in the  co mposed  se rv ice i s  ce rtain t o  be gotten.  Acco rdi ng to  the  definition of a  CSPN, the input place set  P CMI  of a CSPN must b e  e m pty, i.e.  P CM I = .              Theorem 2 :   If a compo s e d  Web  servi c e is execut e d  prop erly, then its co rrespondi ng   CSPN  =  ( P ,  T ,  F ,  M 0 ) is deadlo c k-fre e  e x cept at the end markin g  M ce .  Proof : Acco rding to  defini t ions, A  com posed  We b service  can  b e  exe c uted  p r ope rly if  and o n ly if e a ch  Web  se rvice in th e  co mposed  We b   se rvice   can be  exe c uted  prop erly.  A Web  servi c e i s  ex ecute d  p r ope rly iff its input  passin g  me ssag es  ca n be  gotten a nd it  can  termi nat e  norm a lly. From the two definitions, it can  be inferre d that if a compose d  Web  se rvice is exe c u t ed   prop erly, then  each  Web  se rvice in the co mpo s ed  se rvice ca n term inate normall y.     Proof by cont radi ction is u s ed. Suppo se  the  CSPN  is  deadl ock. It can be inferre d  that a t   least on e of Web  servi c e s  in the compo s ed  Web  se rv ice is n o t executed p r op erl y . However, t h is  con c lu sio n  is contra dicto r y to the above inferen c e fro m  prerequi sit e s. He nce, th e theorem 2 i s   c o rrec t.  Defini tion 9 : C is a path le ading fro m  no de n 1  to n k  iff   a node  seq uen ce <n 1 , n 2 , .. ., n k >  in CS P N s  su ch t hat   (n i , n i+ 1 ) F ,  i=1, 2, ..., k-1. Let &(C) repr esent  the alphabet  of  a path  C, i.e.,  &(C)= { n 1 , n 2 , ..., n k }. C is a n  elem entary  path iff  n i , n j &(C), if i j, n i n j . Node   n j  is  an in heri t or  Evaluation Warning : The document was created with Spire.PDF for Python.
TELKOM NIKA   ISSN:  1693-6 930       Prope rty Anal ysi s of Com p osa b le Web  Servi c e s  (We i  Liu)  737 of nod e n i  i n   C (notation  n i  C n j ) iff   n i ,   n i+1 , ... ,   n j & ( C )  su ch t h at  ( n i , n i+1 ), (n i+1 , n i+ 2 ), ..., (n j-1 ,  n j ) F.   In ou r  study, the  pa ssin g  me ssage  pl ace s  i n   CSPNs a r e  divid ed into  two   cla s ses.   Place s  stan di ng for input p a ssing me ssa ges a r e de no ted by  P CMI  and places  sta nding for o u tput  passin g   me ssag es are de noted  by  P CMO . The sen d i ng tran sition  of place  p  is  denote d  by s( p ).   The re ceivin g  transition of  place  p  is de noted by r( p ).   Theorem 3 :  Let a CSP N  be  com p o s ed  of two d eadlo c k-free  Web  se rvice  pro c e s s  sub net s:  S P N 1  and SPN 2  and  P CMI = . ISPN 1  and ISPN 2  are d ead lock-free except at their e n d   marking. F o r  any elem enta r y path  C j  le a d ing from  i  to  o  in SP N j , j=1, 2, and  l {0 ,1}, there  exists  no pair of pa ssing me ssag e place s   p  an d  q  such that r l+1 ( p ) 1 l C s l+1 ( q ) and r 2-l ( q ) l C 2 s 2-l ( p ) ar e  simultan eou sl y satisfied if the C SPN i s  d eadlo c k-free  except at  M ce .   Proof: In the proof, redu ction to absurdity  is use d . Suppose the con c lu sio n  is not   corre c t,  i.e.,  for som e  ele m entary path   C j  l eadi ng f r om  i  to  o  in  SPN j , j=1,  2,  and l {0,1 }, there   exists som e  pair  of pa ssi ng  me ssage  places  p  a nd  q  su ch t h at   r l+1 ( p ) 1 l C s l+1 ( q ) a nd r 2-l  ( q ) l C 2 s 2-l ( p ) are  si multaneo usly  satisfied. Th at indicate s that there exi s ts the case  such that  SPN l+1  wait s  to re ceive th e pa ssing  m e ssag e of  p  from SP N 2-l  a nd SPN 2-l   waits to receive the  passin g  me ssag e of  q  from SPN l+1 , wh ich i s  called  circul ar  dea dlo ck. In thi s   ca se, s l+1 ( q )  and  s 2- l ( p )  are two  d ead tran sition s, and  the  CSPN is  dea dl ock. But this  con c lu sio n  is  contradi ctory  to   the conditio n  in the theorem 3 that  CSPN is de adlo c k-fre e  except at  M ce . Thereby, the  sup p o s ition is not true and  the Lemma i s  corre c t.  Extend  theor e m  3  to a general  ca se in volving multiple Web  servi c e pro c e ss  su bnets.   Theorem 4 :  Let a CSPN  be co mpo s e d  of n Web  se rvice p r o c e s s subn ets: SPN i , i = 1 ,   ...,  n,  P CMI =  and  ISPN i  is deadl ock-f r ee  except at th eir end ma rki ng.     u,v {1, ... , n}, u v, any   two elem enta r y paths  C u  and C v  leading from  i  to  o  in SPN  u  a nd SPN  v , res p ec tively, there  exists n o  pai r of passin g  m e ssag e pla c e s   p  a nd  q  in   P MI O   such t h a t  f o r k,  l {u, v } , k l, r k ( p )   k C s k ( q ) and  r l ( q )   l C s l ( p ) are sim u ltaneo usly satisfied if the  CSPN is d e a d lock-f ree ex cept at  M ce .   Proof: It is similar to the  theor e m  3 . Bas e d  on  theorem 3 ,  i t  i s  e a s y  t o  v e r i f y  t h e   Theorem 4 .  From  theor e m   3  and  theorem 4 , alth ough th e de adlo ck  of a CSPN d epen ds o n  its  dynamic exe c ution, it i s  e a sy to verify t hat a  CSPN i s  de adlo c k b a se d on th e  net structu r e,  thus  the corre s p o n d ing compo s ed We b se rvic e is n o t executed pro p e r ly based on  theorem 4 .    For the CSP N 1  in Figure  1, SPN 1  and SPN 2  are the two co rre spondi ng We b  service  pro c e s s subn ets of th e  CS PN 1 . In the fo llowing,  we a pply  th eorem  3 a nd  theor e m 4  to  analy z e   the deadl ock-free dom of the CSPN 1 . T he dea dlo c k-freedo m of ISPN 1  and ISPN 2  is obvio us  except at thei r end ma rking .  P MI O = {p 6 , p 7 , p 8 , p 9 }, s(p 6 )=  t 7,  r (p 6 )=  t 2  ,  s ( p 7 )=  t 2,  r(p 7 )= t 8 , s ( p 8 )=  t 3,   r ( p 8 )=  t 6  ,s  (p 9 )= t 6   an d r(p 9 )=  t 4 . In SPN 1 , there  is one  eleme n tary path  lead ing  i  to  o , C 1 =  i 1 t 1  p 2 t 2  p 3 t 3  p 4 t 4 o 1 . In PS 1 , there is one ele m e n tary path, i.e., C 2 = i 2 t 5   p 11 t 6  p 12 t 7  p 13 t 8 o 2 . It is eas y  to verify that  p,  q  P MI O ,  there exists a pair  of   intera ctive int e rface pl aces p 6  an d p 8   su ch t h at  r ( p 6 )= t 2   1 C s(p 8 )=  t 3  a nd r(p 8 )=  t 6 2 C s( p 6 )=  t 7   are  simulta n eou sly sati sfied. Acco rdin g to  th eore m 3 and  th eorem 4 , the CSP N 1  is not   deadl ock-f r ee , thus the co rresp ondi ng co mposed  Web  service ca nn ot be execute d  prop erly.   It is a nece s sary conditi on of ke epin g  deadl ock-f r ee of a CS PN com p o s e d  of n  deadl ock-f r ee  We b  servi c e  pro c e s s  sub nets th at t here is no  ci rcul ar d eadl ock except at  the i r  end markin g s ,  but not a sufficie n t  con d ition.  Fo r ex ample, the   CSPN compo s ed of t w o  Web  servi c e p r o c e ss  sub nets i s  sho w n in Fig u rre 2. For th e CSPN 2  in F i g.2, SPN 3  and SPN 4  are t h e   two  corre s po nding We b service   process subn et s  of the CSP N 2 . T he de adlo c k-f r eed om of IS PN 3   and ISPN 4  i s   easy to  p r ove .  P MI O ={p 8,  p 9,  p 10  },s(p 8 )=  t 4,  r ( p 8 )=  t 2  ,  s (p 9 )= t 3,  r   (p 9 )=  t 5  ,  s ( p 10 )= t 1,   r(p 10 )=  t 6 . In  SPN 3 , there are two el em entary path s   leadin g  from  i  to  o .  C 3 (1) =i 1 t 1 p 3 t 7 o 1 .  C 3 (2) =i 1 t 2  p 2 t 3  p 3 t 7 o 1 . In  SPN 3 ,  there  is  o ne elem entary path, i.e.,  C 4 (1) =i 2 t 4   p 5 t 5 p 6 t 6 o 2 . It is  easy to verify that  p, q P MI O , there  doe s no t evidently exist j {1, 2 }  an d  k { 1 }  su ch th at each of (r 3 (p) () 3 j C p s 3 (q ))   (r 4 (q) () 4 k C p s 4 (p ))  a nd  (r 4 (p)   () 4 k C p s 4 (q))   ( r 3 (q )   () 3 j C p Evaluation Warning : The document was created with Spire.PDF for Python.
                             ISSN: 16 93-6 930   TELKOM NIKA   Vol. 14, No. 2, June 20 16 :  734 – 74 0   738 s 3 (p )) i s  satisf ied. It can be  verified that the CSPN 2  in  Figure 2 is  n o t deadlo c k-free exce pt at its  end ma rki ng.           Figure 1. The  CSPN 1  com p ose d  of SPN 1  and SPN 2  an d their co rrespondi ng ISPN 1  and ISPN 2      i 1 t 1 t 2 P 2 t 3 P 3 t 7 O 1 P 8 P 9 P 10 t 4 P 5 i 2 t 5 P 6 t 6 O 2 CS P N 2 i 1 t 2 P 2 t 3 P 3 t 7 O 1 i 2 t 4 P 5 t 5 P 6 t 6 O 2 SP N 3 SPN 4 IS PN 3 IS PN 4 t 1     Figure 2. The  CSPN 2  com p ose d  of SPN 3  and SPN 4  an d their co rrespondi ng ISPN 3  and ISPN 4      Gene rally, th e de adlo c k-freedom  of a   CSPN  dep en ds  on  not onl y the orde r of  se nding   and  re ceivin g a c tion s a m ong  pro c e s s  sub nets, b u t also the  choi ce  of firi ng  sequ en ce s i n   con d itional ro uting co nstru c ts.   Although it  is  a ne ce ssary   con d ition  of keepi n g  d eadl ock-free  of a   CSPN  co mpo s ed  of n   deadl ock-f r ee  We b service proces s  subnet s at th eir e nd m a rking  that the r e is  no  circular  deadl ock, n o t a  sufficie n t  con d ition, for so me i n te re sting  su bcl a sse s  of  CSPNs, it i s   suffici en t   and ne ce ssa r y con d ition. We focus  on  a cla ss of  CSPNs in which n one of  the sen d ing  and   receiving a c tions i s  incl ude d in any con d i tional routin g  con s tru c tion.   Defini tion 10 :  A Web  se rvice p r o c e ss  subnet  SPN  i s  CC- limited iff    p 1 ,  p 2 P I , if there  exist two  ele m entary  path s   C 1  an d  C 2  (C 1    C 2 ) lea d ing f r om  i  to  o , an d &(C 1 ) &(C 2 )= { p 1 ,  p 2 },   then  t T ( • P MO • P MI ):  t &(C 1 ) &( C 2 ). A  CSP N  i s   CC-limited iff eac h of  its Web  se rvice   p r oc es s   s u bne ts  is  CC- limite d .   Evaluation Warning : The document was created with Spire.PDF for Python.
TELKOM NIKA   ISSN:  1693-6 930       Prope rty Anal ysi s of Com p osa b le Web  Servi c e s  (We i  Liu)  739 Theorem 5:  Let a  CSP N  b e  CC- li mited an d  P CMI = , w h ic h is   c o mp os ed  o f  tw o  deadl ock-f r ee  Web service  process sub nets except a t  their end m a rki n g s : SPN 1  and SPN 2 . For  any elementa r y path C j  lea d ing from  i  to  o  in SPN j , j=1, 2, and l { 0 ,1}, there ex ists no  pair o f   passin g  me ssag e pla c e s   p  and  q   such that r l+1 ( p ) 1 l C s l+1 ( q ) an d r 2-l ( q ) l C 2 s 2-l ( p ) are  simultan eou sl y satisfied iff the CSPN i s   d eadlo c k-free  except at its end ma rki ng.   Sufficiency: S i nce  both  SP N 1  a nd SP N 2   are  de adlo c k-free  exce pt at  their en d m a rkin gs,  the dea dlo c k-freedo m except at its e n d  markin g  of the CSP N  d e pend s o n  the  deadl ock of  the   transitio ns rel a ted to th e pl ace s  i n  P MI O  and th eir  preceden ce  orde r in e a ch  Web  se rvice  p r o c ess  sub net.  However,  the ord e r can not  b e  update d  whe n  a  CSPN is  con s tru c ted, i . e. the st ruct ura l   orde r of the tran sition s in every Web  service p r o c e s s su bnet is th e same a s  that in the CSPN.  Con s e quently ,  when  both Web se rvice pro c e ss su b n e ts are dea dl ock-free in a  CSPN, if the   CSPN i s   not  deadl ock-f r ee , this m ean s  that the in co rrect  order of  the tran sition s  related  to t h e   passin g  messag e pla c e s  in some  Web  servi c e p r o c e ss  sub nets le ads to some  dead tra n sitio n s   in the CSPN.   Becau s e th e  CSPN i s  CC-limited, this  mean s that the sendin g  a nd re ceivin g  passin g   messag e pla c e s  betwe en  SPN 1  and SPN 2  are only in sequ ential  routing  con s truction s in SPN 1  and SPN 2.  By means of th e con d itions  of  the theore m , any elementary path C j  leadin g  from  i  to  o  in SPN j , j = 1 ,  2, and l {0, 1 }, there exi s ts n o  pai r  of p a ssing me ssage  pl aces  p  and  q  such that  r l+1 ( p ) 1 l C s l+1 ( q ) a nd r 2-l ( q ) l C 2 s 2-l ( p ) are sim u ltaneou sly sati sfied. T hat is t o  say, there exist s   no ca se  su c h  t hat  S P N l+1   waits to re ceive the messag e of  p  from SPN 2-l  and SPN 2-l  waits  to  receive the  m e ssag e of  q  from SP N l+1 . Thereby, ea ch tran sition  in  SPN 1  an d S P N 2  is  dea dlo c k- free in the CS PN and the CSPN is dea dl ock-free.    Ne ce ssit y :  C C -limit e d  CS P N  are t he  spe c ial c a s e  of  CS P N s.  S o  t he con c l u sio n  is   corre c t ba sed  on  theor e m 4.   Extend  Theo r em 5  to a general  ca se in volving multiple Web  servi c e pro c e ss  su bnets  Theorem 6 : Let  a CSPN be CC-limited   and  P CMI = , whi c h i s   com posed  of n  d eadlo c k- free We b se rvice pro c e s s sub nets at their end ma rki ngs: SPN i , i  = 1 , ...,  n.   If   u, v {1, .. ., n } ,   u v, ( P MI u P MOu )   (P MI v P MO v )     , an d any two ele m entary path s  C u  and  C v  leadin g  from  i  to  o   in SPN u  and SPN v , respe c tively, there exists no pa ir of passing  message pl ace s   p  and  q  in  P Iu P Iv  s u c h  that for k ,  l {u , v}, k l, r k (p )   k C s k ( q ) and r l ( q )   l C s l ( p ) are  sim u ltaneo usly satisfied  iff the CSPN is dea dlo c k-free exce pt at its end ma rki n g.   Proof: It is  s i milar to the  Theorem 5 . Based on  Th eorem 5 , it is  eas y  to verify the  theore m  6.  A cco rdi ng t o   Theorem 5  and Theor em 6 , a rigorou s an alysis app roa c h  same a s   theor e m 3 a nd the o rem  4  is given  ba sed  on only  static net st ructures  of CSP N s to ve rify the   liveness preservation for  CC-limite d  CS PNs.       4. Conclusio n   The  appli c ati on of S O C  redu ce s the  co mplexity  of bu sine ss  integratio n  within an  enterp r i s e an d across org anization s. To study  the satisfie d pro pertie s  of co mposable  Web  servi c e s , formal model s  based on Pe tri nets a r e  prop osed in  this pap er: the We b serv ice   p r oc es s  ne ts ( SPN s)  r e pre s en tin g  Web  s e r v ic es , th e  in te r n a l  se r v ic e  pr oc es s  ne ts  ( I SPN s )   rep r e s entin g the inne r Web se rvice p r ocess a nd the co mpo s e d  Web  se rvice p r o c e ss  net s  (CSPNs) d e n o ting the  a  compo s ed  We b service.  Ba sed  on th e a bove three fo rmal m odel s,  the  prop ertie s  of  compo s a b le  Web services ar e studi ed. The rel a tions hi p between the pro per  executio n of  We b  servi c e compo s itio n an d inte rface  pa ssing  messa g e s   and  deadl ock of   c o mpos ition work flow  is  disc us sed.If  a  comp os ed Web  s e rvice is executed properly, its   corre s p ondin g  CSPN is  deadl ock-f r ee  except  at  the en d ma rking. To  red u c e  com p lexity of   analysi s ,  the  relation   bet ween a CSPN and  it s  co rre spondi ng We b   se rvice  p r o c ess sub nets are  discu s sed. If the CSPN  compo s ed  of multiple  de ad lock-free We b  se rvice pro c e ss su bnet s  is  deadl ock-f r ee  exce pt their end  markin g s , no  ci rcular deadl ocks e x ist. Althoug h the d eadl o c k- freedo m is a  dynamic  pro p e rty, the prop erty  of deadl o c k-fre edom  can be ju dge d  based on  stat ic  net st ru cture s  by  mea n s  of the  pro p o s ed  meth od s .  Ho wev e r, it is  a  ne ce ss ary  con d it ion .   A   spe c ial  sub c l a ss i s   com e   up  with in  the  pap er, it i s   a  suffici ent a n d  ne ce ssary  con d ition fo r  CC- limited CSPN. Petri nets are also ad opte d  in some  pa pers to model  Web se rvice. Different fro m   Evaluation Warning : The document was created with Spire.PDF for Python.
                             ISSN: 16 93-6 930   TELKOM NIKA   Vol. 14, No. 2, June 20 16 :  734 – 74 0   740 previou s  met hod s, analysi s  metho d s  prese n ted in  thi s  pa per  are  b a se d on the  static stru ctu r e  of  CSPNs.By these meth od s, it is easier to  anal yze  p r op erties  of com posable Web servi c e s .      Ackn o w l e dg ements   This work is supp orted b y  the National Natural Scien c e Fo un dation of Chi na und e r   grant  614 722 28, 611 700 7 8 ; the Natural  Scien c e   Fou ndation  of Sh ando ng p r ovi n ce  und er  grant  ZR20 14FM 0 0 9 , the docto ral pro g ra m o f  higher e d u c ation of the spe c iali zed  rese arch fun d  of  Chin a unde r grant 201 13 7181 1000 4; the Proje c t of Shandon g Province Hig her Edu c atio nal   Scien c e a n d  Tech nolo g y Program un der G r ant  n u m ber  J12 L N11; the Chi n a's Po st-d oct o ral   Scien c e F u n d  unde r g r an t 2012M5 213 62;the Proj ect of Shandon g Post-do c toral Fund  und e r   grant 20 130 3 071;the international  co o peratio n train i ng Proje c t of Shandon g Province Hig h e r  Educatio nal outstan ding  y outh  ba ckbo ne teachers; and Basi c Re se arch Pro g r am of Qing d ao  City of China  unde r grant No. 13-1 - 4-116 -jch.       Referen ces   [1]  Liu J, Lu o  XJ, Li BN, et al. An  Intellig ent Jo b Sc hed uli ng S ystem for Web Service i n  Cl ou d Comp utin g.  T E LKOMNIKA Indon esi an Jou r nal of Electric al Eng i ne eri n g .  2013; 1 1 (6): 2 956- 296 1.   [2]  Liu  W ,  Du YY,  Yan  C. A serv i c e se lect io n m e thod  b a sed  o n  W e b  servic e  Clusters.  Jo u r na l  o f   Ap pl i ed  Scienc e .  2013 ; 13:  5734-5 7 3 8 .  [3]  Maamar Z ,  W i ves LK, Al-K ha tib G, She ng  QZ , et al.  F r om c o mmun itie s of w eb serv i c es to  marts  o f   compos ite w e b serivc es . Pr ocee din g s  of  the 2 4 th IEE E  Internati o n a l  Conf erenc e  on A d vanc ed  Information N e t w ork i n g  and  a pplic atio ns. Pe rth, W A . 2010: 958- 965.    [4]  Liu W ,  Du  YY, Yan  C. A  w e b servic e d i sc over y a nd c o m positi on m e tho d  bas ed  on s e rvice cl asses.  Journ a l of Softw are Engin eer i n g . 201 3; 7: 68 -76.  [5]  Li H, W ang H Y , Cui LZ .  Automatic co mp o s ition of w eb s e rvices b a se d on rul e s an d  meta-s ervic e s .  Procee din g s  o f  the 1 1 th Int e rnati ona l C o n f erenc e  on  C o mputer  Sup p o rted C o o per a t ive W o rk i n   Desig n . Melb o u rne, Vic. 20 07 : 496-50 1.  [6]  Liu W ,  D u  YY , Yan C.  A m e thod  to ca lcu l ate r e comme ndati on trust  o f  W eb servic e s .  Journ a l of  Softw are Engin eeri n g . 20 14; 8 :  108-11 5.  [7] Argenti na  BA.  A mode l-driv en ap proac h to descri be an d pred ict the perfor m a n ce o f  compos it e   services . Proc eed ings of the  6th Internatio nal W o r ksh op  on Soft w a re a nd Performa nc e. Ne w  Y o rk.  200 7: 78-8 9 .  [8]  Liu W ,  D u  YY,  Yan  C. So un dness  pres erv a tion  in  comp o s ed l o g i cal  tim e   w o rkfl o w   net s.  Enterpris e   Information System . 20 12; 6: 95-1 13.   [9]  Liu W ,  Du YY, Z hou MC, Yan C.  T r ansformation of Lo gi cal W o rkflo w   Nets.  IEEE Tr ansactions on  Systems Ma n and Cy bern e tic s : Systems . 20 14; 44(1 0 ): 140 1-14 12.   [10]  Azgomi  MA, E n tezari-M alek i  R. T a sk sched ulin g m o d e ll ing  an d r e li abi lit y  eval uatio n  of g r id s e rvice s   usin g colo ure d  Petri nets.  F u ture Generati on  Co mp uter Systems . 2 010; 2 6 : 1141- 11 50.   [11]  Charfi A, Sch m elin g B, Mezini M.  Reliable messaging  for BPEL processes . IEEE International   Confer ence  on  W eb Services .  Chica go. 20 06 : 293-30 2.  [12] W eera w ar an a  S, Curb era F ,   Le yma nn F ,  St ore y   T ,  F e rgus on  DF .  W eb se rvices  platform  arch itecture:  SOAP, WSDL, WS-polic y ,  W S -addr essin g , WS-BPEL, WS-relia bl e mes s agi ng a nd m o re. Prentice   Hall PT R. 2005 .  [13]  T ang XF , Jia n g  CJ, Z h o u  M C . Automatic  W eb servic e c o mpos ition  bas ed o n  H o rn c l a u ses a nd P e tri  nets.  Expert Systems w i th App licatio ns . 20 11;  38(10): 13 02 4 - 130 31.   [14]  Cambro ner o ME, Díaz G, Valero V, Martínez  E. Validati on a nd v e rificati on of w e b servic es   chore ogra p h i e s  b y   usi ng tim ed a u tomata.  T he Jour nal  of Log ic an d Al g ebra i c Progr a m mi ng . 2 011;  80(1): 25- 49.   [15]  W ang YM. Re search o n  W e b Service C o m positi on Al gorit hm Usin g Des c riptio n Lo gic.  TEL K OMNIKA   Indon esi an Jou r nal of Electric al Eng i ne eri n g .  2014; 1 2 (1): 8 52-8 58.   [16]  Yun BS. F o rmal Mod e li ng  of  T r ust W e b Service C o mpositi on Usi ng Pica lcul us.   TEL K OMNIKA   Indon esi an Jou r nal of Electric al Eng i ne eri n g .  2013; 1 1 (8): 4 385- 439 2.       Evaluation Warning : The document was created with Spire.PDF for Python.