Modelling and verifying web service orchestration by means of the concurrency workbench
- 1 September 2004
- journal article
- Published by Association for Computing Machinery (ACM) in ACM SIGSOFT Software Engineering Notes
- Vol. 29 (5) , 1-10
- https://doi.org/10.1145/1022494.1022526
Abstract
Verification techniques like model checking, preorder checking and equivalence checking are shown to be relevant to web service orchestration. The Concurrency Workbench of the New Century (CWB) is a verification tool that supports these verification techniques. By means of the Process Algebra Compiler (PAC), the CWB is modified to support the BPE-calculus. The BPE-calculus is a small language, based on BPEL4WS, to express web service orchestration. Both the syntax and the semantics of the BPE-calculus are formally defined. These are subsequently used as input for the PAC. As output, the PAC produces modules that are incorporated into the CWB so that it supports the BPE-calculus and, hence, provides a verification tool for web service orchestration.Keywords
This publication has 21 references indexed in Scilit:
- Concurrency and automata on infinite sequencesPublished by Springer Nature ,2005
- Model Checking Multithreaded Programs by Means of Reduced ModelsElectronic Notes in Theoretical Computer Science, 2004
- Modelling and verification of delay-insensitive circuits using CCS and the Concurrency WorkbenchInformation Processing Letters, 2004
- Contracts and typesCommunications of the ACM, 2003
- A Calculus for Long-Running TransactionsPublished by Springer Nature ,2003
- Generic tools for verifying concurrent systemsScience of Computer Programming, 2002
- NUSMV: a new symbolic model checkerInternational Journal on Software Tools for Technology Transfer, 2000
- Modeling and verifying active structural control systemsScience of Computer Programming, 1997
- Testing equivalences for processesTheoretical Computer Science, 1984
- Results on the propositional μ-calculusTheoretical Computer Science, 1983