Verification of Communication Protocols in Web Services

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. INDICE: 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 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

• ISBN: 978-0-470-90539-5
• Editorial: Wiley–Blackwell
• Encuadernacion: Cartoné
• Páginas: 272
• Fecha Publicación: 27/12/2013
• Nº Volúmenes: 1
• Idioma: Inglés