Web服務(wù)線性時(shí)態(tài)邏輯模型檢查研究.pdf

1、江西財(cái)經(jīng)大學(xué)碩士學(xué)位論文Web服務(wù)線性時(shí)態(tài)邏輯模型檢查研究姓名：馮艷清申請(qǐng)學(xué)位級(jí)別：碩士專業(yè)：計(jì)算機(jī)應(yīng)用技術(shù)指導(dǎo)教師：黎升洪20081001A b s t r a c tA s i n g l ea n ds i m p l ew e bs e r v i c e ( W S ) i sd i f f i c u l tt om e e tt h ea c t u a l d e m a n d i nm a n yc a s e s

2、d u e t o t h ec o m p l e x i 夠o fa p p l i c a t i o n s ．T od e a l 謝t l lt h ec o m p l e x b u s i n e s sp r o c e s s e s i tn e e d s t oc o m p o s e a n u m b e r o f W S s ．A n u m b e r o fW S s o f s m a l l

3、g r a n u l a r i t yc o m m u n i c a t ea n d c o l l a b o r a t e w i t l le a c ho t h e r t oa c h i e v ec o m p l e xs e r v i c ef u n c t i o n ．T h ec o m p o s i t i o n o fW S s i S u s e d t o d e s c r i b

4、 e t h e c o m b i n a t i o n o fc r o s s ．o r g a n i z a t i o n a lb u s i n e s s p r o c e s s e s ，s u c ha sh i g h - l e v e l b u s i n e s sl o g i c ，w h i c hm e a n st h a t a n ys y s t e me r r o r sc a

5、i ll e a dt os e v e r el o s s e sa n d f a u l t s ．T h e k e y t o S u c c e s s i st oe n s u r e a n d c o n f i r mt h e v a l i d i t yo f w e b s e r v i c e sc o m p o s i t i o n ．I n t h i s p a p e r m o d e

6、l c h e c k i n g t e c h n o l o g y b a s e d o na u t o m a t a i s a p p l i e d t oc o m p o s i t i o n o f W S s ．F i r s t ，t h es e m a n t i c o f P R O M E L A i ss t u d i e d ．P R O M E L A l a n g u a g ei

7、st h e c o r eo f t h e S P I Nt o o l ，t h eu n d e r s t a n d i n go fP R O M E L A i m p l e m e n t a t i o ni st h ed e c i s i o n t o t h eb e h a v i o ro f t h es y s t e m ．T h ef o r m a l d e f i n i t i o n

8、o ft h eo b j e c tm o d e lo fP R O M E L A s y n t a xa n d a na l g o r i t h ma r e g i v e n t oa c h i e v eP R O M E L A a b s t r a c ts y n t a xt om a p t h e o b j e c t m o d e l ，d e s c r i b e s t h e d e

9、n o t a t i o n a l s e m a n t i c s o fP R O M E L A ．T h ec o m p l e xi s s u e ss u c h a sa t o m i ca n d s y n c h r o n o u s c o m m u n i c a t i o n a r e g i v e n t h es o l u t i o n ．T h e n f o r m a lm

10、o d e l i n ga n d v e r i f i c a t i o nw i t h P R O M E L A b a s e d o n t h eW S ．C D L a r ep r o p o s e d ．T h ef l o w c o n t r o lm e c h a n i s m ss u p p o r t e db yW S - C D L i n c l u d e s ：s e q u e

11、n c e ，p a r a l l e l ，s y n c h r o n i z a t i o n ，n o n —d e t e r m i n i s t i c c h o i c e ，e t e ．W e p r o p o s e am o d e l i n gp r o c e d u r e t h a tp r e s e r v e st h ec o n t r o l f l o wa n d t h

12、e d a t af l o w o f W S —C D L p r o c e s s m o d e l s ，w h i c h C a l ld e t e c ti n c o r r e c t i n t e r a c t i o n b e t w e e n c o n t r o l f l o wa n d d a t a f l o w ．T h em a p p i n go fW S —C D L t o

13、P R O M E L A h i n g e so nt h ed e c i s i o no fw h i c ha s p e c t so f t h eW S ．C D Lp r o c e s sm o d e la r et o ( a n dc a n ) b ee x p r e s s e di nP R O M E L A ，a n do nh o w t op e r f o r ms u c h a m a

14、p p i n g ．F i n a l l yu s i n gm o d e lc h e c k i n gt o o l S P I Nt o a n a l y s i s t h eo n —l i n e t r a d i n g w h i c hs u p p o r t e db ya t h i r dp a r t y ．T h ee x p e r i m e n tp r o v e dt h a tt h

15、 ep r o c e d u r ec a n b e e f f e c t i v ef o rt h ev e r i f i c a t i o no f W e b s e r v i c e sb a s e d o n t h e W S ．C D L ．K e y w o r d s ：W e b S e r v i c e s ；L i n e a rT e m p o r a l L o g i c ；F o r