Kazi Sakib, Zahir Tari, Peter Bertók
Verification of Communication Protocols in Web Services
Model-Checking Service Compositions
Kazi Sakib, Zahir Tari, Peter Bertók
Verification of Communication Protocols in Web Services
Model-Checking Service Compositions
- Gebundenes Buch
- Merkliste
- Auf die Merkliste
- Bewerten Bewerten
- Teilen
- Produkt teilen
- Produkterinnerung
- Produkterinnerung
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.
Andere Kunden interessierten sich auch für
- Mark I. MontrosePrinted Circuit Board Design Techniques for EMC Compliance183,99 €
- Timothy RooneyIpv6 Deployment and Management94,99 €
- Vijay KumarFundamentals of Pervasive Information Management Systems116,99 €
- Jun ZhengWireless Sensor Networks140,99 €
- S. S. IyengarFundamentals of Sensor Network Programming140,99 €
- Fernando S. ParreirasSemantic Web and Model-Driven Engineering92,99 €
- Gerard Meijer (ed.)Smart Sensor Systems116,99 €
-
-
-
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.
Produktdetails
- Produktdetails
- The Wiley Series on Parallel and Distributed Computing
- Verlag: Wiley & Sons
- 1. Auflage
- Seitenzahl: 272
- Erscheinungstermin: 4. Dezember 2013
- Englisch
- Abmessung: 241mm x 159mm x 20mm
- Gewicht: 592g
- ISBN-13: 9780470905395
- ISBN-10: 0470905395
- Artikelnr.: 30627347
- The Wiley Series on Parallel and Distributed Computing
- Verlag: Wiley & Sons
- 1. Auflage
- Seitenzahl: 272
- Erscheinungstermin: 4. Dezember 2013
- Englisch
- Abmessung: 241mm x 159mm x 20mm
- Gewicht: 592g
- ISBN-13: 9780470905395
- ISBN-10: 0470905395
- Artikelnr.: 30627347
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.
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
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
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
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