Behavioural Theory at Work: Program Transformations in a Service-Centred Calculus

We analyse the relationship between object-oriented modelling and session-based, service-oriented modelling, starting from a typical UML Sequence Diagram and providing a program transformation into a service-oriented model. We also provide a similar transformation from session-based specifications into request-response specifications. All transformations are specified in SSCC--a process calculus for modelling and analysing service-oriented systems--and proved correct with respect to a suitable form of behavioural equivalence (full weak bisimilarity). Since the equivalence is proved to be compositional, results remain valid in arbitrary contexts.