Verification of Communication Protocols in Web Services: Model-Checking Service Compositions -- Copyright -- Contents -- Preface -- 1 INTRODUCTION: SERVICE RELIABILITY -- 1.1 Motivation -- 1.2 Technical Challenges -- 1.3 Summary of Earlier Solutions -- 1.4 Summary of New Ways to Verify Web Services -- 1.5 Structure of the Book -- References -- 2 MODEL CHECKING -- 2.1 Advantages and Disadvantages of Model Checking -- 2.2 State-Space Explosion -- 2.3 Model-Checking Tools -- References -- 3 PETRI NETS -- 3.1 Colored Petri Nets -- 3.1.1 CPN ML -- 3.1.2 CPN Syntax and Semantics -- 3.1.3 Timed Colored Petri Nets -- 3.1.4 Multisets -- 3.1.5 CPN Definitions -- 3.2 Hierarchical Colored Petri Nets -- References -- 4 WEB SERVICES -- 4.1 Business Process Execution Language -- 4.2 Spring Framework -- 4.3 JAXB 2 APIs -- 4.3.1 Unmarshaling XML Documents -- 4.3.2 Marshaling Java Objects -- References -- 5 MEMORY-EFFICIENT STATE-SPACE ANALYSIS IN SOFTWARE MODEL CHECKING -- 5.1 Motivation -- 5.2 Overview of the Problem and Solution -- 5.3 Related Work -- 5.4 Models for Memory-Efficient State-Space Analysis -- 5.4.1 Sequential Model -- 5.4.2 Tree Model -- 5.5 Experimental Results -- 5.6 Discussion -- 5.7 Summary -- References -- 6 TIME-EFFICIENT STATE-SPACE ANALYSIS IN SOFTWARE MODEL CHECKING -- 6.1 Motivation -- 6.2 Overview of the Problem and Solution -- 6.3 Overview of Hierarchical Colored Petri Nets -- 6.4 Related Work -- 6.5 Technique for Time-Efficient State-Space Analysis -- 6.5.1 Access Tables and Parameterized Reachability Graph -- 6.5.2 Exploring a Module -- 6.5.3 Access Table and Parameterized Reachability Graph for a Super-module -- 6.5.4 Algorithms for Generating Access Tables and Parameterized Reachability Graphs -- 6.5.5 Additional Memory Cost for Storing Access Tables and Parameterized Reachability Graphs.

6.5.6 Theoretical Evaluation of the Reduction in Delay -- 6.6 Experimental Results -- 6.7 Discussion -- 6.8 Summary -- References -- 7 GENERATING HIERARCHICAL MODELS BY IDENTIFYING STRUCTURAL SIMILARITIES -- 7.1 Motivation -- 7.2 Overview of the Problem and Solution -- 7.3 Basics of Substitution Transition -- 7.4 Related Work -- 7.5 Method for Installing Hierarchy -- 7.5.1 Lookup Method -- 7.5.2 Clustering Method -- 7.5.3 Time Complexity of the Lookup Algorithm -- 7.6 Experimental Results -- 7.7 Discussion -- 7.8 Summary -- References -- 8 FRAMEWORK FOR MODELING, SIMULATION, AND VERIFICATION OF A BPEL SPECIFICATION -- 8.1 Motivation -- 8.2 Overview of the Problem and Solution -- 8.3 Related Work -- 8.4 Colored Petri Net Semantics for BPEL -- 8.4.1 Component A -- 8.4.2 Component B -- 8.4.3 Object Model for BPEL Activities -- 8.4.4 XML Templates -- 8.4.5 Algorithm for Cloning Templates -- 8.5 Results -- 8.6 Discussion -- 8.7 Summary -- References -- 9 CONCLUSIONS AND OUTLOOK -- 9.1 Results -- 9.2 Discussion -- 9.3 What Could Be Improved? -- References -- INDEX.