Verification of Communication Protocols in Web Services: Model-Checking Service Compositions

INDEX

Access table 9, 117–18, 126–9, 134–45, 152

memory cost 143–5

super module 134–7

Automaton 8, 20, 27, 84, 209

Backtracking 79, 89

Binding 38, 53, 121, 131, 214

compiler 74, 214

partial 131

partial compatible 137–8

Business Process Execution Language (BPEL) 3, 57, 59–70

activities 60–70

synchronisation of concurrent activities 68

delays 65

event handling 67

fault handling 66

partner links 60

verification 5, 8, 9, 205–42

Clustering method 157, 159, 162, 189–93, 203

Compositional reasoning 21

Compound place 54, 122–3

Data transfer object (DTO) 3, 74–5, 207, 246, 248–9, 252

Dead-path elimination (DPE) 207, 209, 210, 223, 228

Decrease-and-conquer 156–7, 159, 163, 203

Difference form 8, 87–8, 95–8, 100–101, 107, 112

Difference state 79, 89, 98, 104, 112, 113

Document type definition (DTD) 55, 208, 221, 235, 242

Duplicate state 20, 80, 84

Dynamic service composition 2, 59, 209

Elementary group 170, 176, 194

Exhaustive storage 7, 19–20, 78, 85

False negative 85, 250

False positive 85, 250

Formal methods 3, 16, 77, 205, 207, 249

Formal representation 31, 156, 158, 250

Graph isomorphism problem 116, 124

Graph-encoded tuple set 20, 85

Group 170, 172, 176–7

Hash function 91, 94, 96, 100, 103, 165, 167

Hash table 81, 83, 91–4, 100–101, 103, 164–8, 172–5, 178–9, 193–4, 202

Indegree 159, 164

Lookup method 157, 159, 163–88, 201–2

Marshaling 74–5, 214

Metagroup 177, 180

Model flat 6, 11, 155–8, 246

hierarchical 3, 9, 11, 117–18, 155–203

Model checking compositional 155

Modeling language ...