Verification of Communication Protocols in Web Services Model-checking Service Compositions

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.

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

MODEL CHECKING 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 CHECKING 115

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 a

Super-module / 134

6.5.4 Algorithms for Generating Access Tables and Parameterized

Reachability Graphs / 137

6.5.5 Additional Memory Cost for Storing Access Tables and

Parameterized 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

STRUCTURAL SIMILARITIES 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 BPEL SPECIFICATION 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

The New copy of this book will include any supplemental materials advertised. Please check the title of the book to determine if it should include any access cards, study guides, lab manuals, CDs, etc.

The Used, Rental and eBook copies of this book are not guaranteed to include any supplemental materials. Typically, only the book itself is included. This is true even if the title states it includes any access cards, study guides, lab manuals, CDs, etc.