Web Services and Formal Methods
7th International Workshop, WS-FM 2010, Hoboken, NJ, USA, September 16-17, 2010. Revised Selected Papers
Published on 19. March 2011
VIII, 191 pages
978-3-642-19589-1 (ISBN)
Description
This book constitutes the thoroughly refereed post-workshop proceedings of the 7th International Workshop on Web Services and Formal Methods, WS-FM 2010, held in Hoboken, NJ, USA, in September 2010. The 11 revised full papers presented together with one invited paper were carefully reviewed and selected from 26 submissions. The papers feature topics such as web services; service oriented computing; cloud computing; formal methods; verification specification; testing; and business process management.
More details
Other editions
Additional editions
Mario Bravetti | Tevfik Bultan
Web Services and Formal Methods
7th International Workshop, WS-FM 2010, Hoboken, NJ, USA, September 16-17, 2010. Revised Selected Papers
Book
03/2011
Springer
€53.49
Shipment within 7-9 days
Content
- Title
- Preface
- Organization
- Table of Contents
- Introducing the Guard-Stage-Milestone Approach for Specifying Business Entity Lifecycles
- Introduction
- Overview of Project ArtiFact
- The Guard-Stage-Milestone Meta-model
- Information Models
- Overview of Lifecycle Models
- Stage and Milestone Status
- Events and Sentries
- Milestones
- Stage Bodies and Atomic Stages
- Illustration of Derived Attributes
- Guards
- Macros for Activity Flow Constructs
- Sub-stages
- BEL Service Centers (BSC's)
- Parallelism, Transactional Consistency, and Attribute Status
- Exception Handling
- Macros and Design Patterns
- GSM Operational Semantics
- Transformation into ECA Rules
- Examples
- Representative Verification and Reasoning Problems
- Related Work
- Conclusions
- References
- Simplified Computation and Generalization of the Refined Process Structure Tree
- Introduction
- Preliminaries
- The Refined Process Structure Tree
- The Triconnected Components
- Simplified Computation of the Refined Process Structure Tree
- The RPST of Normalized TTGs
- The RPST of General TTGs
- Generalization of the Refined Process Structure Tree
- The RPST of TTGs
- The RPST of MTGs
- Conclusion
- References
- Automated Generation of Web Service Stubs Using LTL Satisfiability Solving
- Introduction
- Web Service Stubs
- A Running Example
- Producing a Web Service Stub
- Current Solutions
- A Formal Model of Web Service Stub Behaviour
- First-Order Linear Temporal Logic: LTL-FO+
- Formalizing Web Service Constraints
- Model Checking and Satisfiability of LTL-FO+
- An Off-the-Shelf Web Service Stub
- Tool Chain
- From a Trace to a Kripke Structure
- From LTL-FO+ to LTL
- Experimental Results
- Conclusion and Open Issues
- References
- Passive Testing of Web Services
- Introduction
- Preliminaries
- Invariants
- Local Invariants
- Global Invariants
- Conclusions and Future Work
- References
- On Lifecycle Constraints of Artifact-Centric Workflows
- Introduction
- Motivations
- ArtiNet: A Formal Model for Artifact-Centric Workflows
- Lifecycle Constraints of Artifacts
- Compliance of Lifecycle Constraints
- Workflow Construction from Lifecycle Specification
- Conclusions
- References
- Conformance Verification of Privacy Policies
- Introduction
- Overview of Security Policies
- PV Framework
- Data Model
- Web Application
- Action
- Modeling Security Policy
- Conformance Verification Problem
- Verification
- Overview
- Translating PV Transition System to Alloy
- Translating CTL-FO Formula
- Initial Experimental Results
- Static Information Flow Analysis
- Path Transducer
- Static Analysis for Constructing Transition System
- Related Work
- Conclusion
- References
- Generalised Computation of Behavioural Profiles Based on Petri-Net Unfoldings
- Introduction
- Background
- Net Syntax and Semantics
- Unfoldings of Net Systems
- Behavioural Profiles
- Generalised Computation of Behavioural Profiles
- Behavioural Relations
- Computation Algorithm
- Experimental Evaluation
- Behavioural Profile of a Labelled Net System
- Related Work
- Conclusion
- References
- Constructing Replaceable Services Using Operating Guidelines and Maximal Controllers
- Introduction
- Preliminaries
- Services and Controllers
- Accordance Preorder and Equivalence
- Operating Guidelines
- Accordance-Preserving Transformation Rules
- Maximal Controller
- Finite Maximal Controllers
- Construction
- Validity
- Canonicity
- Applications to Service Replaceability
- Deciding Replaceability
- Characterizing all Replaceable Services
- Constructing a Public View of a Service
- Related Work
- Conclusion and Further Work
- References
- Soundness-Preserving Refinements of Service Compositions
- Introduction
- Preliminaries
- Petri Nets, Workflows and Soundness
- Open Nets and Composition
- Accordance
- Synchronizable Places
- Introduction
- Soundness
- Refinement with the Simplest Synchronizing Net
- Some Transitions Should Not Occur
- Some Transitions Should Occur
- Homogeneous Solution
- Refinement in Terms of Composition
- Two Checks for Soundness
- Generalizing Theory
- Foundation
- Computing Maximal Controllers
- Conclusions and Further Work
- References
- Formal Semantics and Implementation of BPMN 2.0 Inclusive Gateways
- Introduction
- BPMNinc and Its Informal Semantics
- Sequence Flow and Tokens
- Exclusive Gateways
- Inclusive Gateways
- Start and End Events
- Formal Semantics for BPMNinc
- BPMNinc Process Graphs
- BPMNinc Formal Semantics
- Incremental and Distributed Implementations
- Related Work
- Conclusion and Future Work
- References
- Failure Analysis for Composition of Web Services Represented as Labeled Transition Systems
- Introduction
- Illustrative Example
- MoSCoE Composition Algorithm
- Web Services as Transition Systems
- The Service Composition Problem
- Failure Analysis for MoSCoE Composition
- Tree of Recovery Options
- Identifying Recovery Options
- Case Study
- Conclusion
- References
- On Nondeterministic Workflow Executions
- Introduction
- Organization Flow
- Workflows and Executions
- Management of Workflow Executions
- Fully Distributed Workflows
- Transformation Flow
- Conclusions
- References
- Author Index
