Motivation

• WS-CDL Critical Success Factors
• CSF-007
  • To be successful, a CDL description MUST be verifiable at runtime
• CSF-008
  • To be successful, a CDL description MUST enable static verification of correctness properties

Why Formalism?

• To provide mechanisms for ensuring desirable properties of real systems (e.g. Type checking, Bi-simulation, Model checking)
  • CSF-008 requires static type checking for behavioural types
• To give unambiguous semantics to WS-CDL so that we have a precise idea of behaviour, offering guidelines for implementation
  • CSF-007 requires formal semantics to ensure correct monitoring

Correctness

• What formalism can we use for this?
• We need:
  • Mobility
  • Concurrency
  • Location
  • Identity (of a conversation)
• Process algebra provides the basis for all of this with a few additions

Formalisms

π-calculus

• A program’s state and its “program pointer” are one and the same
• Completely does away with the representation of state
• It is easy to check for certain properties
  • Deadlock
  • Compatibility
• Linear Typing to support safety/liveness properties in the presence of non-determinism and non-termination

π-calculus

• Formally we have:
• 
• where e ::= v|x|f(e1, …., ek).

Example

π-calculus

• And we also have an end point calculus:
  • Just as readable as before, but the point is ...
• 

References

• [1] Carbone, Honda, Yoshida
• “Programming Interaction with Types”
• [2] Kavantzas
• “Aggregating Web Services: Choreography and WS-CDL”
• [3] Carbone, Honda, Yoshida, et. al.
• “A Theoretical Basis of Communication-Centred Concurrent Programming”
• [4] Milner, Parrow, Walker
• “A Calculus of Mobile Processes”

Resources

• W3C Web Services Choreography page: http://www.w3.org/2002/ws/chor
• This talk linked from http://www.w3.org/Talks/
• Pi4SOA has an available implementation of CDL editors, endpoint generators: http://www.pi4soa.org