Formal semantics and analysis of control flow in WS-BPEL

DOI10.1016/J.SCICO.2007.03.002MaRDI QIDQ997228zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Chun Ouyang, Eric Verbeek, W. M. P. van der Aalst, Stephan Breutel, Marlon Dumas, Arthur H. M. ter Hofstede

Publication date 23 July 2007

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://eprints.qut.edu.au/14809/1/14809.pdf

zbMATH Keywords

Petri netsBPELWeb servicesbusiness process modelingtool-based verification

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• A formal model for BPEL4WS description of Web service composition
• Model transformation and formal verification for semantic web services composition
• A Language for Reliable Service Composition
• Model-checking web services orchestrations using BP-calculus
• Fundamental Approaches to Software Engineering

Cited in

(18)

• Reo + \(\mathrm{mCRL2}\): a framework for model-checking dataflow in service compositions
• A formal model for BPEL4WS description of Web service composition
• Session types for safe web service orchestration
• A WSDL-based type system for asynchronous WS-BPEL processes
• A formal model for service-oriented interactions
• Computer Aided Verification
• A formal semantics for the Taverna 2 workflow model
• An algebraic theory for web service contracts
• Model transformation and formal verification for semantic web services composition
• Ontology-driven analysis of UML-based collaborative processes using OWL-DL and CPN
• Compositional Specification of Web Services Via Behavioural Equivalence of Nets: A Case Study
• What Do Semantics Matter When the Meat Is Overcooked?
• On the potential advantages of exploiting behavioural information for contract-based service discovery and composition
• A Language for Reliable Service Composition
• Monotonicity in Service Orchestrations
• Monitoring and recovery for web service applications
• Efficient semantics-based compliance checking using LTL formulae and unfolding
• Model-checking web services orchestrations using BP-calculus

Describes a project that uses

Uses Software

• Woflan
• BPEL2PN
• YAWL
• WSAT

This page was built for publication: Formal semantics and analysis of control flow in WS-BPEL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q997228)