Web Services and Formal Methods
8th International Workshop, WS-FM 2011, Clermont-Ferrand, France, September 1-2, 2011, Revised Selected Papers
Published on 23. April 2012
IX, 143 pages
978-3-642-29834-9 (ISBN)
Description
This book constitutes the thoroughly refereed post-proceedings of the 8th International Workshop on Web Services and Formal Methods, WS-FM 2011, held in Clermont-Ferrand, France, in September 2011. The workshop was co-located with the 9th International Conference on Business Process Management, BPM 2011.
The 9 full papers presented were carefully reviewed and selected from 14 submissions. They deal with service oriented computing (SOC), cloud computing and formal methods.
More details
Other editions
Additional editions
Marco Carbone | Jean-Marc Petit
Web Services and Formal Methods
8th International Workshop, WS-FM 2011, Clermont-Ferrand, France, September 1-2, 2011, Revised Selected Papers
Book
04/2012
Springer
€53.49
Shipment within 7-9 days
Content
- Title
- Preface
- Organization
- Table of Contents
- Understanding Distributed Servicesthrough the \pi-Calculus
- Reliable Contracts for Unreliable Half-Duplex Communications
- Asynchronous Dialogues
- Contracts
- Half-Duplex Dialogues
- LTL Model-Checking
- Traces of Configurations
- Traces of Actions
- Conclusion
- References
- Behavior Based Service Composition
- Introduction
- Formal Framework
- Service Advertisements
- Programs
- Query Logic for Specifying Composed Behavior
- Solution to the Synthesis Problem
- Computing Constraints on Transition Relation
- Synthesizing Deterministic Crash-Free Programs
- Example
- Related Work
- References
- Compatibility of Data-Centric Web Services
- Introduction
- Distributed Active Documents
- Modeling Active Documents Workflows with Petri Nets
- Documents and Services
- Docnets
- Modules and Interactions with the Environment
- Composability
- Compatibility between Modules
- Connecting Interfaces and Their Implementations
- Distributivity of Compatibility
- Conclusion and Perspectives
- References
- Time and Exceptional Behavior in Multiparty Structured Interactions
- Introduction
- The Conversation Calculus (CC)
- C3: CC with Time and Compensations
- The Expressiveness of C3, Informally
- A Healthcare Compelling Example
- Related Work
- Concluding Remarks
- References
- Toward Design, Modelling and Analysis of Dynamic Workflow Reconfigurations
- Introduction
- Office Workflow: Requirements and Design
- Requirements
- Design
- Asynchronous -Calculus
- Web
- Discussion
- References
- An Operational Semantics of BPEL Orchestrations Integrating Web Services Resource Framework
- Introduction
- Background and Related Work
- Overview of BPEL/WSRF
- Related Work
- Syntax and Semantics of BPEL+RF
- Case Study: Online Auction Service
- Conclusions and Future Work
- References
- Design of a BPEL Verification Tool
- Introduction
- A Brief Overview of BPEL and FIACRE
- BPEL
- FIACRE
- Transformation Framework
- Transformation Basis
- Camlp4 and FIACRE Meta-extensions
- From BPEL to FIACRE
- Transformation Principles
- Modeling the WSDL
- Behavioral Aspects in FIACRE
- Common Behavior of Activities in FIACRE:
- Basic Activities.
- Structured Activities.
- Verification
- Case Study
- Related Works
- BPEL Verification Tools
- Comparison of Transformation Environments
- Conclusion and Future Work
- References
- Applying Process Analysis to the Italian eGovernment Enterprise Architecture
- Introduction
- Business Process Management
- The Process Monitoring Platform
- Formal Analysis Based on Petri Nets
- Using Invisible Transitions to Improve Performance Analysis
- Supporting BPMN Modeling
- Citizen Migration
- Integrating ProM in the Process Monitoring Platform
- Concluding Remarks
- References
- Domain-Specific Multi-modeling of Security Concerns in Service-Oriented Architectures
- Introduction
- Integrating the Non-functional Concerns
- A Framework for the Inclusion of Security Concerns
- Development Process
- Metamodels
- WS-I's Supply Chain Management Use Case
- Creating and Selecting the Input Models
- Transformation into the iMM Model
- Generation of Resulting Artifacts
- Related Work
- Conclusions and Future Work
- References
- Author Index
