Preface |
|
xi | |
1 Introduction: Service Reliability |
|
1 | (14) |
|
|
4 | (1) |
|
|
5 | (2) |
|
1.3 Summary of Earlier Solutions |
|
|
7 | (1) |
|
1.4 Summary of New Ways to Verify Web Services |
|
|
8 | (2) |
|
1.5 Structure of the Book |
|
|
10 | (1) |
|
|
11 | (4) |
2 Model Checking |
|
15 | (12) |
|
2.1 Advantages and Disadvantages of Model Checking |
|
|
18 | (1) |
|
2.2 State-Space Explosion |
|
|
19 | (3) |
|
|
22 | (3) |
|
|
25 | (2) |
3 Petri Nets |
|
27 | (30) |
|
|
31 | (18) |
|
|
31 | (4) |
|
3.1.2 CPN Syntax and Semantics |
|
|
35 | (6) |
|
3.1.3 Timed Colored Petri Nets |
|
|
41 | (6) |
|
|
47 | (1) |
|
|
47 | (2) |
|
3.2 Hierarchical Colored Petri Nets |
|
|
49 | (6) |
|
|
55 | (2) |
4 Web Services |
|
57 | (20) |
|
4.1 Business Process Execution Language |
|
|
59 | (11) |
|
|
70 | (4) |
|
|
74 | (2) |
|
4.3.1 Unmarshaling XML Documents |
|
|
74 | (1) |
|
4.3.2 Marshaling Java Objects |
|
|
75 | (1) |
|
|
76 | (1) |
5 Memory-Efficient State-Space Analysis In Software Model Checking |
|
77 | (38) |
|
|
78 | (1) |
|
5.2 Overview of the Problem and Solution |
|
|
79 | (4) |
|
|
83 | (3) |
|
5.4 Models for Memory-Efficient State-Space Analysis |
|
|
86 | (22) |
|
|
87 | (11) |
|
|
98 | (10) |
|
|
108 | (4) |
|
|
112 | (1) |
|
|
113 | (1) |
|
|
113 | (2) |
6 Time-Efficient State-Space Analysis In Software Model Checking |
|
115 | (40) |
|
|
116 | (2) |
|
6.2 Overview of the Problem and Solution |
|
|
118 | (1) |
|
6.3 Overview of Hierarchical Colored Petri Nets |
|
|
119 | (4) |
|
|
123 | (2) |
|
6.5 Technique for Time-Efficient State-Space Analysis |
|
|
125 | (24) |
|
6.5.1 Access Tables and Parameterized Reachability Graph |
|
|
126 | (3) |
|
|
129 | (5) |
|
6.5.3 Access Table and Parameterized Reachability Graph for a Super-module |
|
|
134 | (3) |
|
6.5.4 Algorithms for Generating Access Tables and Parameterized Reachability Graphs |
|
|
137 | (6) |
|
6.5.5 Additional Memory Cost for Storing Access Tables and Parameterized Reachability Graphs |
|
|
143 | (2) |
|
6.5.6 Theoretical Evaluation of the Reduction in Delay |
|
|
145 | (4) |
|
|
149 | (2) |
|
|
151 | (1) |
|
|
152 | (1) |
|
|
153 | (2) |
7 Generating Hierarchical Models By Identifying Structural Similarities |
|
155 | (50) |
|
|
156 | (2) |
|
7.2 Overview of the Problem and Solution |
|
|
158 | (2) |
|
7.3 Basics of Substitution Transition |
|
|
160 | (1) |
|
|
161 | (1) |
|
7.5 Method for Installing Hierarchy |
|
|
162 | (32) |
|
|
163 | (26) |
|
|
189 | (4) |
|
7.5.3 Time Complexity of the Lookup Algorithm |
|
|
193 | (1) |
|
|
194 | (7) |
|
|
201 | (1) |
|
|
202 | (1) |
|
|
203 | (2) |
8 Framework For Modeling, Simulation, And Verification Of A BPEL Specification |
|
205 | (40) |
|
|
206 | (2) |
|
8.2 Overview of the Problem and Solution |
|
|
208 | (1) |
|
|
209 | (2) |
|
8.4 Colored Petri Net Semantics for BPEL |
|
|
211 | (25) |
|
|
211 | (3) |
|
|
214 | (3) |
|
8.4.3 Object Model for BPEL Activities |
|
|
217 | (4) |
|
|
221 | (13) |
|
8.4.5 Algorithm for Cloning Templates |
|
|
234 | (2) |
|
|
236 | (5) |
|
|
241 | (1) |
|
|
242 | (1) |
|
|
242 | (3) |
9 Conclusions And Outlook |
|
245 | (10) |
|
|
246 | (3) |
|
|
249 | (2) |
|
9.3 What Could Be Improved? |
|
|
251 | (1) |
|
|
252 | (3) |
Index |
|
255 | |