This post originated from an RSS feed registered with Java Buzz
by Paul Brown.
Original Post: More on BPEL and Formalism
Feed Title: mult.ifario.us
Feed URL: http://feeds.feedburner.com/MultifariousCategoryJava
Feed Description: Software. Business. Java. XML. Web Services.
I talked some about formalism and BPEL on 2004-02-22.Satish Thatte (from Microsoft) posted a message on the WS-BPEL TC mailing list about some work on BPEL formal semantics, this time using Abstract State Machines ("ASM"). (Microsoft has some tooling for working with ASM; it has been applied, e.g., to COM and .NET. It can also be applied to concurrency in Java.)The paper, from Roozbeh Farahbod, Uwe Glässer and Mona Vajihollahi, is motivated by Issue 42 (OASIS membership required for the link):There is a need for formalism. It will allow us to not only reason about the current specification and related issues, but also uncover issues that would otherwise go unnoticed. Empirical deduction is not sufficient. Other efforts have begun to formalize their language (i.e. XQUERY).
It provides explicit models for BPEL activities in terms of ASM. The paper makes for interesting reading (if you're into that kind of thing, which I am), but it's disappointing that the paper appears to focus on the BPEL4WS 1.1 specification (which will be obsoleted when the OASIS specification is released later this year) and doesn't treat the more interesting and challenging aspects, namely variables, faults, and compensation.I expect and hope to see Issue 42 remain unresolved in so far as imposing any particular formalism and any specific level of granularity on BPEL. The fact that BPEL is amenable to formal analysis is sufficient, and so far, people have successfully modeled it with Petri nets, pi-calculus, and ASM. (I have yet to see a complete model in the academic literature, but there are complete formal representations in some commercial implementations, e.g., ours.)I've added a new snip on Academic work on BPEL with a collection of links to various academic papers.
I'm interested in modelization and verification of BPEL and looking for any document that defines a formal semantic, essentially in pi-calculus. Does anyone have any idea of a location? Thanks.
Previous Topic
