Verification of communication protocols in web services model-checking service compositions
"Provides implementation details of each networking type to help readers to be able to set up Sensor networks in their related job fields"--
| Otros Autores: | , , |
|---|---|
| Formato: | Libro electrónico |
| Idioma: | Inglés |
| Publicado: |
Hoboken, New Jersey :
Wiley
[2014]
|
| Edición: | 1st edition |
| Colección: | Wiley series on parallel and distributed computing ;
83 |
| Materias: | |
| Ver en Biblioteca Universitat Ramon Llull: | https://discovery.url.edu/permalink/34CSUC_URL/1im36ta/alma991009627738206719 |
Tabla de Contenidos:
- 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.
