Choreographic specifications and potential testing and validation relati

I mentioned that I would supply some pointers to sample documents that discuss some aspect of the relation of specifications and implementations as these distinctions apply to choreography (public process specfications) and orchestration (private process executions process descriptions or implementation instructions).

Examples of standards that are concerned with specifications of public process are ebBP 2.0 and UML 2.1 sequence diagrams. Possibly also WS-CDL.

Examples of standards concerned with descriptions tied to private process implementation include BPMN 1.1 ( a graphical notation that some have compiled under special restrictions into an execution or implementation format) and WS-BPEL.

[BPMN 2.0 is supposed to somehow merge the specification and implementation perspectives on public and private process, and it is to be hoped that it is successful.]

Here is a presentation of work by Frank Puhlmann and Mathias Weske at Hasso Plattner Institut that provides a vision of how implementation descriptions (or even code) might be related to specification level descriptions, at design time (a static checking of implementation conforming with specification).

http://bpt.hpi.uni-potsdam.de/pub/Public/FrankPuhlmann/InteractionSoundness.pdf

The above approach uses model theoretic techniques for its checking process. Specifically, bisimulation is used to check on model fidelity of implementation with specification.

Approaches that relate events could be viewed as also a check on specific execution traces viewed as models in accordance with ideas underlying the above reference.

Or the relation of execution event traces to specifications might make use of token style approaches to simulation/testing. The YAWL work from Australia and Netherlands might provide an indication of that way of construing event traces to specifications.

See for example the end of (the reservations about pi calculus illustrate a dispute concerned with applied research that is perhaps instructive for us to note)

http://is.tm.tue.nl/research/patterns/download/pi-hype.pdf

YAWL papers and code resources (alleged to handle even the difficult token vacuum cleaning issues for workflow cancellation patterns) is at

http://www.yawl-system.com/

tamie message