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

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 ...