Verification of Communication Protocols in Web Services: Model-Checking Service Compositions / Edition 1 available in Hardcover
- Pub. Date:
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.
|Series:||Wiley Series on Parallel and Distributed Computing Series , #83|
|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.
Table of Contents
PREFACE xi1 INTRODUCTION: SERVICE RELIABILITY 11.1 Motivation 41.2 Technical Challenges 51.3 Summary of Earlier Solutions 71.4 Summary of New Ways to Verify Web Services 81.5 Structure of the Book 10References 112 MODEL CHECKING 152.1 Advantages and Disadvantages of Model Checking 182.2 State-Space Explosion 192.3 Model-Checking Tools 22References 253 PETRI NETS 273.1 Colored Petri Nets 313.1.1 CPN ML 313.1.2 CPN Syntax and Semantics 353.1.3 Timed Colored Petri Nets 413.1.4 Multisets 473.1.5 CPN Definitions 473.2 Hierarchical Colored Petri Nets 49References 554 WEB SERVICES 574.1 Business Process Execution Language 594.2 Spring Framework 704.3 JAXB 2 APIs 744.3.1 Unmarshaling XML Documents 744.3.2 Marshaling Java Objects 75References 765 MEMORY-EFFICIENT STATE-SPACE ANALYSIS IN SOFTWARE MODELCHECKING 775.1 Motivation 785.2 Overview of the Problem and Solution 795.3 Related Work 835.4 Models for Memory-Efficient State-Space Analysis 865.4.1 Sequential Model 875.4.2 Tree Model 985.5 Experimental Results 1085.6 Discussion 1125.7 Summary 113References 1136 TIME-EFFICIENT STATE-SPACE ANALYSIS IN SOFTWARE MODEL CHECKING1156.1 Motivation 1166.2 Overview of the Problem and Solution 1186.3 Overview of Hierarchical Colored Petri Nets 1196.4 Related Work 1236.5 Technique for Time-Efficient State-Space Analysis 1256.5.1 Access Tables and Parameterized Reachability Graph 1266.5.2 Exploring a Module 1296.5.3 Access Table and Parameterized Reachability Graph for aSuper-module 1346.5.4 Algorithms for Generating Access Tables and ParameterizedReachability Graphs 1376.5.5 Additional Memory Cost for Storing Access Tables andParameterized Reachability Graphs 1436.5.6 Theoretical Evaluation of the Reduction in Delay 1456.6 Experimental Results 1496.7 Discussion 1516.8 Summary 152References 1537 GENERATING HIERARCHICAL MODELS BY IDENTIFYING STRUCTURALSIMILARITIES 1557.1 Motivation 1567.2 Overview of the Problem and Solution 1587.3 Basics of Substitution Transition 1607.4 Related Work 1617.5 Method for Installing Hierarchy 1627.5.1 Lookup Method 1637.5.2 Clustering Method 1897.5.3 Time Complexity of the Lookup Algorithm 1937.6 Experimental Results 1947.7 Discussion 2017.8 Summary 202References 2038 FRAMEWORK FOR MODELING, SIMULATION, AND VERIFICATION OF A BPELSPECIFICATION 2058.1 Motivation 2068.2 Overview of the Problem and Solution 2088.3 Related Work 2098.4 Colored Petri Net Semantics for BPEL 2118.4.1 Component A 2118.4.2 Component B 2148.4.3 Object Model for BPEL Activities 2178.4.4 XML Templates 2218.4.5 Algorithm for Cloning Templates 2348.5 Results 2368.6 Discussion 2418.7 Summary 242References 2429 CONCLUSIONS AND OUTLOOK 2459.1 Results 2469.2 Discussion 2499.3 What Could Be Improved? 251References 252INDEX 255