Verification of communication protocols in web services : model-checking service compositions

Verification of communication protocols in web services : model-checking service compositions / Zahir Tari, Peter Bertok, Anshuman Mukherjee, RMIT University.

"Provides implementation details of each networking type to help readers to be able to set up Sensor networks in their related job fields"--

Saved in:
Bibliographic Details
Main Author: Mukherjee, Anshuman
Other Authors: Tari, Zahir, Bertók, Péter, 1952-
Format: eBook
Language:English
Published: Hoboken, New Jersey : John Wiley & Sons, 2013.
Series:Wiley series on parallel and distributed computing ; 83
Subjects:
Web services > Testing.
Computer network protocols.
COMPUTERS > Computer Engineering.
Computer network protocols
Online Access:Click for online access
Table of Contents:
  • 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 Definitions3.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 SOFTWAREMODEL 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 SOFTWAREMODEL CHECKING6.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 aSuper-module; 6.5.4 Algorithms for Generating Access Tables and ParameterizedReachability Graphs; 6.5.5 Additional Memory Cost for Storing Access Tables and Parameterized Reachability Graphs.
  • 6.5.6 Theoretical Evaluation of the Reduction in Delay6.6 Experimental Results; 6.7 Discussion; 6.8 Summary; References; 7 GENERATING HIERARCHICAL MODELS BY IDENTIFYINGSTRUCTURAL 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 Solution8.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.

Similar Items