ISBN-10:
0470905395
ISBN-13:
9780470905395
Pub. Date:
12/04/2013
Publisher:
Wiley
Verification of Communication Protocols in Web Services: Model-Checking Service Compositions / Edition 1

Verification of Communication Protocols in Web Services: Model-Checking Service Compositions / Edition 1

Hardcover

Current price is , Original price is $129.0. You

Temporarily Out of Stock Online

Please check back later for updated availability.

Product Details

ISBN-13: 9780470905395
Publisher: Wiley
Publication date: 12/04/2013
Series: Wiley Series on Parallel and Distributed Computing Series , #83
Pages: 272
Product dimensions: 6.20(w) x 9.30(h) x 0.80(d)

About the Author

ZAHIR TARI, PhD, is Professor in Distributed Systems atthe Royal Melbourne Institute of Technology (RMIT University), andhead of the Distributed Systems and Networking group at the Schoolof Computer Science and IT. He is the author of two books, editorof over four, and has been published in numerous prestigiousjournals and conferences.

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

Anshuman Mukherjee teaches at the Institute ofInformation Technology, University of Dhaka in Bangladesh. He haspublished multiple works on sensor networking in addition toauthoring one book on the subject.

Read an Excerpt

Click to read or download

Table of Contents

PREFACE xi

1 INTRODUCTION: SERVICE RELIABILITY 1

1.1 Motivation 4

1.2 Technical Challenges 5

1.3 Summary of Earlier Solutions 7

1.4 Summary of New Ways to Verify Web Services 8

1.5 Structure of the Book 10

References 11

2 MODEL CHECKING 15

2.1 Advantages and Disadvantages of Model Checking 18

2.2 State-Space Explosion 19

2.3 Model-Checking Tools 22

References 25

3 PETRI NETS 27

3.1 Colored Petri Nets 31

3.1.1 CPN ML 31

3.1.2 CPN Syntax and Semantics 35

3.1.3 Timed Colored Petri Nets 41

3.1.4 Multisets 47

3.1.5 CPN Definitions 47

3.2 Hierarchical Colored Petri Nets 49

References 55

4 WEB SERVICES 57

4.1 Business Process Execution Language 59

4.2 Spring Framework 70

4.3 JAXB 2 APIs 74

4.3.1 Unmarshaling XML Documents 74

4.3.2 Marshaling Java Objects 75

References 76

5 MEMORY-EFFICIENT STATE-SPACE ANALYSIS IN SOFTWARE MODELCHECKING 77

5.1 Motivation 78

5.2 Overview of the Problem and Solution 79

5.3 Related Work 83

5.4 Models for Memory-Efficient State-Space Analysis 86

5.4.1 Sequential Model 87

5.4.2 Tree Model 98

5.5 Experimental Results 108

5.6 Discussion 112

5.7 Summary 113

References 113

6 TIME-EFFICIENT STATE-SPACE ANALYSIS IN SOFTWARE MODEL CHECKING115

6.1 Motivation 116

6.2 Overview of the Problem and Solution 118

6.3 Overview of Hierarchical Colored Petri Nets 119

6.4 Related Work 123

6.5 Technique for Time-Efficient State-Space Analysis 125

6.5.1 Access Tables and Parameterized Reachability Graph 126

6.5.2 Exploring a Module 129

6.5.3 Access Table and Parameterized Reachability Graph for aSuper-module 134

6.5.4 Algorithms for Generating Access Tables and ParameterizedReachability Graphs 137

6.5.5 Additional Memory Cost for Storing Access Tables andParameterized Reachability Graphs 143

6.5.6 Theoretical Evaluation of the Reduction in Delay 145

6.6 Experimental Results 149

6.7 Discussion 151

6.8 Summary 152

References 153

7 GENERATING HIERARCHICAL MODELS BY IDENTIFYING STRUCTURALSIMILARITIES 155

7.1 Motivation 156

7.2 Overview of the Problem and Solution 158

7.3 Basics of Substitution Transition 160

7.4 Related Work 161

7.5 Method for Installing Hierarchy 162

7.5.1 Lookup Method 163

7.5.2 Clustering Method 189

7.5.3 Time Complexity of the Lookup Algorithm 193

7.6 Experimental Results 194

7.7 Discussion 201

7.8 Summary 202

References 203

8 FRAMEWORK FOR MODELING, SIMULATION, AND VERIFICATION OF A BPELSPECIFICATION 205

8.1 Motivation 206

8.2 Overview of the Problem and Solution 208

8.3 Related Work 209

8.4 Colored Petri Net Semantics for BPEL 211

8.4.1 Component A 211

8.4.2 Component B 214

8.4.3 Object Model for BPEL Activities 217

8.4.4 XML Templates 221

8.4.5 Algorithm for Cloning Templates 234

8.5 Results 236

8.6 Discussion 241

8.7 Summary 242

References 242

9 CONCLUSIONS AND OUTLOOK 245

9.1 Results 246

9.2 Discussion 249

9.3 What Could Be Improved?  251

References 252

INDEX 255 

Customer Reviews

Most Helpful Customer Reviews

See All Customer Reviews