On TGG Ability for Transforming UML 2 Sequence Diagrams with Imbricate Combined Fragments to π-Calculus Specifications

This paper describes a way based on operational semantics of π-calculus and uses TGG tool to formalize sequence diagrams to establish formal verification through model transformations. Our transformation uses basic interactions and combined fragments with the operator Alt, Opt and Par. We argue that TGG rules can be more easily used and they become more understandable. The transformation feasibility is illustrated on a scenario of phone system.