Muutke küpsiste eelistusi

Verification of Communication Protocols in Web Services: Model-Checking Service Compositions [Kõva köide]

(The Royal Melbourne Institute of Technology, Australia), ,
Teised raamatud teemal:
Teised raamatud teemal:
In the near future, wireless sensor networks will become an integral part of our day-to-day life. To solve different sensor networking related issues, researchers have been putting various efforts and coming up with innovative ideas. Within the last few years, we have seen a steep growth of research works particularly on various sensor node organization issues. The objective of this book is to gather recent advancements in the fields of self-organizing wireless sensor networks as well as to provide the readers with the essential information about sensor networking.
Preface xi
1 Introduction: Service Reliability 1(14)
1.1 Motivation
4(1)
1.2 Technical Challenges
5(2)
1.3 Summary of Earlier Solutions
7(1)
1.4 Summary of New Ways to Verify Web Services
8(2)
1.5 Structure of the Book
10(1)
References
11(4)
2 Model Checking 15(12)
2.1 Advantages and Disadvantages of Model Checking
18(1)
2.2 State-Space Explosion
19(3)
2.3 Model-Checking Tools
22(3)
References
25(2)
3 Petri Nets 27(30)
3.1 Colored Petri Nets
31(18)
3.1.1 CPN ML
31(4)
3.1.2 CPN Syntax and Semantics
35(6)
3.1.3 Timed Colored Petri Nets
41(6)
3.1.4 Multisets
47(1)
3.1.5 CPN Definitions
47(2)
3.2 Hierarchical Colored Petri Nets
49(6)
References
55(2)
4 Web Services 57(20)
4.1 Business Process Execution Language
59(11)
4.2 Spring Framework
70(4)
4.3 JAXB 2 APIs
74(2)
4.3.1 Unmarshaling XML Documents
74(1)
4.3.2 Marshaling Java Objects
75(1)
References
76(1)
5 Memory-Efficient State-Space Analysis In Software Model Checking 77(38)
5.1 Motivation
78(1)
5.2 Overview of the Problem and Solution
79(4)
5.3 Related Work
83(3)
5.4 Models for Memory-Efficient State-Space Analysis
86(22)
5.4.1 Sequential Model
87(11)
5.4.2 Tree Model
98(10)
5.5 Experimental Results
108(4)
5.6 Discussion
112(1)
5.7 Summary
113(1)
References
113(2)
6 Time-Efficient State-Space Analysis In Software Model Checking 115(40)
6.1 Motivation
116(2)
6.2 Overview of the Problem and Solution
118(1)
6.3 Overview of Hierarchical Colored Petri Nets
119(4)
6.4 Related Work
123(2)
6.5 Technique for Time-Efficient State-Space Analysis
125(24)
6.5.1 Access Tables and Parameterized Reachability Graph
126(3)
6.5.2 Exploring a Module
129(5)
6.5.3 Access Table and Parameterized Reachability Graph for a Super-module
134(3)
6.5.4 Algorithms for Generating Access Tables and Parameterized Reachability Graphs
137(6)
6.5.5 Additional Memory Cost for Storing Access Tables and Parameterized Reachability Graphs
143(2)
6.5.6 Theoretical Evaluation of the Reduction in Delay
145(4)
6.6 Experimental Results
149(2)
6.7 Discussion
151(1)
6.8 Summary
152(1)
References
153(2)
7 Generating Hierarchical Models By Identifying Structural Similarities 155(50)
7.1 Motivation
156(2)
7.2 Overview of the Problem and Solution
158(2)
7.3 Basics of Substitution Transition
160(1)
7.4 Related Work
161(1)
7.5 Method for Installing Hierarchy
162(32)
7.5.1 Lookup Method
163(26)
7.5.2 Clustering Method
189(4)
7.5.3 Time Complexity of the Lookup Algorithm
193(1)
7.6 Experimental Results
194(7)
7.7 Discussion
201(1)
7.8 Summary
202(1)
References
203(2)
8 Framework For Modeling, Simulation, And Verification Of A BPEL Specification 205(40)
8.1 Motivation
206(2)
8.2 Overview of the Problem and Solution
208(1)
8.3 Related Work
209(2)
8.4 Colored Petri Net Semantics for BPEL
211(25)
8.4.1 Component A
211(3)
8.4.2 Component B
214(3)
8.4.3 Object Model for BPEL Activities
217(4)
8.4.4 XML Templates
221(13)
8.4.5 Algorithm for Cloning Templates
234(2)
8.5 Results
236(5)
8.6 Discussion
241(1)
8.7 Summary
242(1)
References
242(3)
9 Conclusions And Outlook 245(10)
9.1 Results
246(3)
9.2 Discussion
249(2)
9.3 What Could Be Improved?
251(1)
References
252(3)
Index 255
ZAHIR TARI, PhD, is Professor in Distributed Systems at the Royal Melbourne Institute of Technology (RMIT University), and head of the Distributed Systems and Networking group at the School of Computer Science and IT. He is the author of two books, editor of over four, and has been published in numerous prestigious journals and conferences.

PETER BERTOK researches and lectures on networked and distributed systems at RMIT University. He has over 100 publications for conferences and journals and has written numerous book chapters. He is vice chair of the IFIP Working Group on Co-operation Infrastructure for Virtual Enterprises and Electronic Business, and is a member of the IEEE and the ACM.

Anshuman Mukherjee teaches at the Institute of Information Technology, University of Dhaka in Bangladesh. He has published multiple works on sensor networking in addition to authoring one book on the subject.